8

I have this minimal working example (culled from the singletons library) of mapping a type family over a type-level list:

{-# language PolyKinds #-}
{-# language DataKinds #-}
{-# language TypeFamilies #-}
{-# language TypeOperators #-}

data TyFun :: * -> * -> *

data TyCon1 :: (k1 -> k2) -> (TyFun k1 k2 -> *)

type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
type instance Apply (TyCon1 f) x = f x

type family Map (f :: TyFun a b -> *) (as :: [a]) :: [b] where
    Map f '[] = '[]
    Map f (x ': xs) = Apply f x ': Map f xs

type family Flip t :: * where
    Flip Int = Char
    Flip Char = Int

It seems to work:

ghci> :set -XDataKinds
ghci> :kind! Map (TyCon1 Flip) '[Char,Int]
Map (TyCon1 Flip) '[Char,Int] :: [*]
= '[Int, Char]

The code is explained in the post Defunctionalization for the win. It is a workaround for the fact that "GHC will not let a type variable unify with a type family". This is called the "saturation requirement of type families".

My doubt is: when we "run" :kind! Map (TyCon1 Flip) '[Char,Int] it seems that , in the line type instance Apply (TyCon1 f) x = f x, f will be matched with our Flip type family. Why doesn't this infringe the saturation requirement?

danidiaz
  • 26,936
  • 4
  • 45
  • 95
  • I don't think that's supposed to work. However, it's perfectly harmless because the synonyms are expanded in type checking. – dfeuer Nov 23 '16 at 19:22
  • 1
    I believe you're really supposed to provide a defunctionalization symbol for `Flip` with its own `Apply` instance. `TyCon1` is intended to be applied to type constructors. By the way, what version of GHC is this? – dfeuer Nov 23 '16 at 19:24
  • 1
    @dfeuer I'm using GHC 8.0.1. Apparently, the thing works when using `:kind!` in ghci, but if I try to add something like `type Boo = Map (TyCon1 Flip) '[Char,Int]` to the script, it gives me a compilation error. – danidiaz Nov 23 '16 at 20:00
  • 1
    @dfeuer When you say "you're really supposed to provide a defunctionalization symbol for Flip" do yo mean something like `data FlipSym :: TyFun * * -> *`, `type instance Apply FlipSym x = Flip x`? This way seems to work. – danidiaz Nov 23 '16 at 20:06
  • Yes, that sounds right. I don't know why `kind!` behaves like that. – dfeuer Nov 23 '16 at 20:34
  • @dfeuer You could put those comments in an answer so that I could accept it. – danidiaz Nov 23 '16 at 20:42
  • 2
    @dfeuer `kind!` behaves like so because `:kind! SomeTypeFamily` is supposed to work, even when the type family isn't fully applied - but clearly this rule shouldn't be applied to sub-expressions, only to the outer application, in the thing occurring to the right of `:kind!`. It would seem this is a bug in GHCi. – user2407038 Nov 23 '16 at 21:47

1 Answers1

2

I'm answering my own question with information culled from dfeuer and user2407038's comments.

Turns out that my code did infringe the saturation requirement. I didn't find the error because of a strange behaviour (bug?) of :kind! in ghci. But writing the type in the hs file itself gives a compilation error.

TyCon1 is not for type families, but for wrapping regular type constructors like Maybe, that have no problem unifying with type variables. type Foo = Map (TyCon1 Maybe) '[Char,Int] works fine, for example.

For type families, we need to define a special auxiliary type for each of them, and then define an Apply instance for the type. Like this:

data FlipSym :: TyFun * * -> *
type instance Apply FlipSym x = Flip x

type Boo = Map FlipSym '[Char,Int]

Notice that this way the Flip type family is not unifying with any type variable.

danidiaz
  • 26,936
  • 4
  • 45
  • 95
  • 1
    Sorry I didn't get around to putting up an answer myself. Yours is at least as good as what I'd have written. One nit I'd like to pick: I don't like the name `Flip` for that family. In my mind, that name is always defined `newtype Flip (f :: j -> k -> *) (y :: k) (x :: j) = Flip { unFlip :: f x y }`. The resulting type-level version of `flip` comes up fairly often, and generally in contexts where the type synonym version (`type Flip f y x = f x y`) would not be useful. – dfeuer Nov 24 '16 at 23:03