[Haskell-cafe] Promotion of field accessors using DataKinds
adam at well-typed.com
Mon Jan 11 13:05:51 UTC 2016
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 , 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
> 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
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
More information about the Haskell-Cafe