So I've done this...
{-# LANGUAGE Rank2Types, GADTs #-}
type Record fields = forall t. fields t -> t
data PersonField t where
Name :: PersonField String
Age :: PersonField Int
type Person = Record PersonField
And then this...
nigel :: Person
nigel Name = "Nigel"
nigel Age = 39
And it all seems to work as expected.
What I'm struggling with is how to define a Person value inside a let binding. For example this doesn't work:
abigail :: Person
abigail = let x Name = "Abigail"
x Age = 27
in x
Gives me:
Couldn't match expected type `t1' with actual type `[Char]' `t1' is untouchable ...
Is there a way to make this work inside a let binding?
You need explicit type annotations when GADTs are involved:
abigail :: Person
abigail = let x :: Person
x Name = "Abigail"
x Age = 27
in x
Without it, GHC roughly sees
let x Name = "Abigail"
and says "OK, x
is a function from the type of Name
, i.e. PersonField String
to the type of "Abigail"
, i.e. String
. In the next line,
let x Name = "Abigail"
x Age = 27
GHC now finds out x
to accept also a PersonField Int
and to return a number. This clashes with the previously inferred type, triggering a type error.
With an explicit type annotation, type inference will not try to infer a wrong type for x
: it was provided by the user. Instead, only type checking will be performed.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With