Search code examples
recordstype-kindspurescript

Records in PureScript

I don't quite understand why this works:

module Records where

type Element e = { element :: String, label :: String | e }
type Sel = ( value :: Number, values :: [Number] )

type Select = Element Sel

while this says Cannot unify # * with *.

module Records where

type Element e = { element :: String, label :: String | e }
type Sel = { value :: Number, values :: [Number] }

type Select = Element Sel

(Note the '()' around the right hand side of Sel instead of the '{}'.)

I've read here https://leanpub.com/purescript/read#leanpub-auto-objects-and-rows that forall r. { firstName :: String, lastName :: String | r } desugars to forall r. Object (firstName :: String, lastName :: String | r)

I'm still a bit confused, why you can't use the record-sugar for extending records.

Solution

  • The Object type constructor is parameterized by a row of types. In kind notation, Object has kind # * -> *. That is, it takes a row of types to a type.

    ( value :: Number, values :: [Number] ) denotes a row of types (something of kind # *), so it can be passed to Object to construct a type, namely

    Object ( value :: Number, values :: [Number] )

    Note that { ... } is just syntactic sugar for the Object type constructor, so this is the same as 

    { value :: Number, values :: [Number] }

    Both have kind *, so it doesn't make sense to pass this thing as an argument to Element, since the type variable e in Element has kind # *.

    Put another way, Element Sel in your second example unrolls to

    { element :: String, label :: String | { value :: Number, values :: [Number] } }

    which desugars to

    Object (element :: String, label :: String | Object (value :: Number, values :: [Number]) )

    which fails to kind-check due to the thing of kind * in the tail of the outer row.