TypeData declarations arrived in GHC 9.6 (March 2023), aimed at building on DataKinds aka data type promotion
… which means that a single data declaration introduces both a type with value constructors, and a kind with type constructors. In some cases this alleviates the need for duplicated declarations (e.g., Bool ), however, in many common cases using promotion leads to clutter.
That is, the cluttering of namespaces with data constructors intended never to be used in terms.
I’m trying to follow the proposal and discussion from early 2018. It’s hard to cast memory back to what was and wasn’t in GHC at the time. There’s
What I notice there is TypeRepr, explained in the module top-comments:
-- In addition, we provide a value-level reification of the type
-- indices that can be examined by pattern matching, called 'TypeRepr'.
So there is something to be used in terms?? As well as the type data constructors to be used as types and the type data (emm) type to be used as kind type-of-type. The canonical style of declaration is given in the Proposed Change:
type data Universe = Character | Number | Boolean
data Type u where
Character :: Type Character
Number :: Type Number
Boolean :: Type Boolean
This corresponds (I think) to a technique in the HList paper (2004 – so waaay before any promoting was allowed [**] – Section 4 Type-level naturals)
class HNat n
data HZero; instance HNat HZero
data HSucc n; instance HNat n => HNat (HSucc n)
hZero :: HZero; hZero = ⊥
hSucc :: HNat n => n -> HSucc n; hSucc _ = ⊥
hPred :: HNat n => HSucc n -> n; hPred _ = ⊥
-- example usage
hLookupByHNat hZero (id .*. HNil) ...
-- "Numeral-based access operations for heterogeneous collections"
What does it gain with an EmptyDataDecl then making hZero = ⊥ to give a term-level name, as opposed to (say) data HZero = MkHZero to give a term-level name?
Although type data constructor (type) Number has only value ⊥, GADT Number :: Type Number is a legitimate non-bottom value. Then term name Number can be used in pattern matching as well as a function parameter(?)
Is there a more general design pattern here? To have three layers of naming:
type-of-type Universe
type Number
term Number (I’m carefully following the example here; I can see that duplicate name won’t work in a unified namespace; so NumberProxy??)
Then in the type data decl should there be the ability to declare all three layers together?
[**] Then class HNat is ‘poor person’s promotion’ to be able to group the Peano constructors/constrain them from other type-level constructors.
The use of EmptyDataDecls like this was a common pre-DataKinds trick to create type-level “data constructors”. I guess the author used ⊥ instead of an actual constructor to emphasize that HZero was only intended to be used as a type-level construct, not to provide information for use at runtime. Then hZero fulfills the function of Proxy, allowing a “type argument” to be passed.
Of course this isn’t hugely safe, e.g. if your caller gives you a HZero argument nothing stops you eliminating it using EmptyCase, and you need tricks like HNat to regain some level of “kind checking”. Hence the motivation for doing this more robustly with DataKinds.
I’d be careful here: the type data constructor Number is not a “type” in the sense of “a thing that classifies values”. Thus saying that ⊥ :: Number is a kind error, just as ⊥ :: Maybe is a kind error.
The word “type” is sometimes used to mean “a thing that uses the type-level namespace”, but I think it’s clearer to use phrases such as “type constructor” or “type-level expression” for those. Thus the type data constructor Number is not a type, but it is a type-level expression. Similarly Maybe is not (strictly) a type, but it is a type constructor.
One way to think about this is to observe that the Type datatype defined here is really the “singleton type” corresponding to Universe. Given a (type-level) datatype, the singleton construction gives a mechanical way to construct a corresponding datatype for use at the term level, such that pattern matching on the singleton corresponds to dependent pattern matching.
Maybe. One can certainly automate generation of the singleton type from the original, e.g. as in the singletons package. But that’s really a workaround for being unable to use dependent pattern matching directly.
From a dependent types perspective, there should ideally be one type that can be used at both levels. Much as in the pre-DataKinds days we used EmptyDataDecls to fake DataKinds, today we can use singletons to fake dependent types, subject to various awkward constraints such as needing two datatypes for what is conceptually a single type. Perhaps in the future such hacks may become unnecessary.
Does the TypeData extension make the reflection package superfluous? See this question. That is, does it become easier to get our hands on functions with types like
We have Maybe :: Type -> Type, so yes that’s not a type simpliciter. Is Maybe Number a type; or is it ill-formed (ill-kinded because Number :: Universe)?
Should your sentence read “the type data constructor Number is not a Type”? (By lower-case ‘type’ usually I mean anything that can come after a :: in a term’s annotation, or as an ‘argument’ to function arrow ->.)
Thank you Adam for a comprehensive reply. “unnecessary” when we have (I’m guessing)
hLookupByHNat :: forall (l :: HList). forall (n :: HNat) -> l -> hElemByHNat n l
-- ^^^^^^ dependent quant
-- example usage
hLookupByHNat HZero (id .*. HNil) ...
-- ^^^^^ type, not term
in which (l :: HList) is a heterogeneous list, so the type of its nth element depends on the n so gets calculated by type-level function hElemByHNat (that I invented out of thin air). This dependency is expressed in the original FunDep in hLookupByHNat’s method decl.
And to call the function, I didn’t need a term-level hZero. OTOH (l :: HList) is needed both for its (element) type(s) to calculate the result type from hLookupByHNat and for its term-level value to yield the nth term. So I’m not sure that signature is happy.
I’m afraid I still don’t grok what the singletons package is all about. It was presented as a temporary work-around, so I decided to skip it and wait for the proper approach.
Not really. TypeData allows one to define data constructors that can only be used at the type level, not at the term level. But for mixing levels one still needs singletons / dependent types.
A proxy doesn’t carry any runtime information, so forall (b :: Bool) . Proxy b -> Bool isn’t able to return different values at different types. That’s where some form of singleton is needed (sometimes expressed using a class constraint, e.g. forall (b :: Bool) . SingI b => Proxy b -> Bool). With visible dependent quantification (in recent GHCs) this can be simplified to forall (b :: Bool) -> SingI b => Bool. Full dependent types in the future may allow foreach (b :: Bool) -> Bool, where the foreach quantifier indicates that the value is passed at runtime rather than being erased.
Indeed, Maybe Number ill-kinded (whichever Number is being used).
My sentence uses “type” the way I think it should be used. But the important thing is to recognise that there are two possible meanings and be clear about which one is being used in any particular context. (Your definition is roughly what I mean by “type-level expression”.)
Okay, I can sort of see that. It would violate parametricity.
But how is this different, then? The class constraint is an implicit dictionary parameter. How does that contain more run-time information about b than the Proxy? Is it because the Sing type family provides structured values to pattern-match on? (Sorry, I did not mean to turn this thread into a singletons tutorial.)
Still I think extensions like DataKinds or TypeData ought to be bundled with some of the functionality that singleton’s demote provides. It currently doesn’t because there is no suitable type class in base or GHC lib?
Yes, the dictionary for SingI b is ultimately just a value of type SBool b, which provides both a runtime value isomorphic to Bool and a proof of the equality between the value passed at runtime and the type-level Bool:
data SBool (b :: Bool) where
SFalse :: SBool False
STrue :: SBool True
But the important thing is to recognise that there are two possible meanings and be clear about which one is being used in any particular context. (Your definition is roughly what I mean by “type-level expression”.)