[Haskell-cafe] Promotion of field accessors using DataKinds

9 Jan 2016

      Hello all,

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

Now,

    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?

Thanks,
Will

[Haskell-cafe] Promotion of field accessors using DataKinds

William Yager