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
- Example of real code where the clutter is a problem: crucible/crucible/src/Lang/Crucible/Types.hs at master · GaloisInc/crucible · GitHub
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 makinghZero = ⊥
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⊥
, GADTNumber :: Type Number
is a legitimate non-bottom value. Then term nameNumber
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; soNumberProxy
??)
- type-of-type
- 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.