[Haskell-cafe] Promotion of field accessors using DataKinds
will.yager at gmail.com
Sat Jan 9 23:23:26 UTC 2016
Let's say I have some data
data Config = Conf (len :: Nat) (turboEncabulate :: Bool)
Using DataKinds, we can promote Config to a kind and Conf to a type.
However, it does not appear that GHC supports e.g.
data Thing (conf :: Config) = Thing
data Count (n :: Nat) = Count
foo :: Thing conf -> Count (len conf)
foo Thing = Count
That is, it does not appear to properly replace "len conf" with the value
of len from conf.
Instead, the way I've found to do this is to define
class Lengthed (a :: Config) where
type Len a :: Nat
instance Lengthed (Conf n) where
type Len (Conf n t) = n
foo :: Thing conf -> Count (Len conf)
works fine. So manually defining a type function that intuitively does the
exact same thing as "len" seems to work.
Is there a particular reason behind this?
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe