[Haskell-cafe] Promotion of field accessors using DataKinds

[Adam Gundry]

Hi Will,

On 09/01/16 23:23, William Yager wrote:
>     data Config = Conf (len :: Nat) (turboEncabulate :: Bool)

> 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.

Indeed, this is not yet supported. GHC doesn't currently have any form
of promotion for functions (as opposed to datatypes), including record
selectors. Thus when `len` is used in a type, it always refers to a type
variable, not a function.

You might be interested in the singletons package [1], which
automatically generates promoted functions using Template Haskell. A
full treatment of function promotion is an open research problem,
because it requires reconciling the non-trivial differences between
term-level functions and type families (which aren't really functions at
all). In the meantime, your only options are separately defining type
families corresponding to functions, either manually or via TH.


> 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.

Do note that the class isn't really necessary here: you could simply define

    type family Len (c :: Config) :: Nat where
      Len (Conf n t) = n

Best regards,

Adam

[1] http://hackage.haskell.org/package/singletons


-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/