Opened 4 years ago

Last modified 4 years ago

#10776 new feature request

DataKinds promotion of String -> Symbol and Natural -> Nat

Reported by: htebalaka Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.10.2
Keywords: DataKinds Cc: dmcclean
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #11342 Differential Rev(s):
Wiki Page:

Description (last modified by htebalaka)

Exactly what it says on the tin. It would be nice if the following would compile:

{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}

import GHC.TypeLits
import GHC.Natural

data X = X String Natural

data Y :: X -> * where
    Y :: Y ('X "hello" 4)

I kind of assume there's already a ticket for this, but couldn't find one, so figured I'd open one in case.

Change History (5)

comment:1 Changed 4 years ago by htebalaka

Description: modified (diff)

comment:2 Changed 4 years ago by goldfire

Combining Natural and Nat seems straightforward. But Symbol and String are different: the former is not a list of characters. Symbol is much more like a promoted Text than a promoted String. And we might want the kind String to mean a type-level list of type-level characters someday.

Even better than making progress on these small issues is to step back and come up with a plan for type-level literals of all stripes (floating-point numbers, characters, a promoted Num class of some sort?). I'm worried that small forays into this space will dig us into a local minimum from which we can't escape.

comment:3 Changed 4 years ago by dmcclean

A hearty amen on this one, especially unifying Natural with Nat.

Regarding the String objection perhaps it would be better to merely flesh out Symbol at the term level? With an IsString instance and so forth? Because as mentioned unifying it with String is problematic since String is a type synonym for a list of characters.

I also agree with Richard's comments regarding the desirability of type-level literals of all stripes (or at least other stripes). I'm not sure if floating-point numbers or characters specifically are useful, but integers and rationals most definitely are of use to the dimensional library. We have home-brewed ones, but it is a lot of machinery, isn't interoperable with the few other flavors of home-brewed ones on the market, and isn't the lifted version of Rational or Integer so you can't use the lifted kinds that go with the types of term-level structures that include rational or integers.

comment:4 Changed 4 years ago by dmcclean

Cc: dmcclean added

comment:5 Changed 4 years ago by thomie

Note: See TracTickets for help on using tickets.