Understanding the casts involved in patterns matching a datatype that is indexed over a user defined kind

So, I was playing around with DataKinds and TypeFamilies in Haskell and started to look at the Core GHC generated.

Here is a little TestCase to motivate my question:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

module TestCase where

data Ty = TyBool | TyInt

type family InterpTy (t :: Ty) :: *
type instance InterpTy TyBool = Bool
type instance InterpTy TyInt  = Int

data Expr (a :: Ty) where
  I :: Int  -> Expr TyInt
  B :: Bool -> Expr TyBool

eval :: Expr a -> InterpTy a
eval (I i) = i
eval (B b) = b

Let's take a look at the generated Core for the eval function

TestCase.eval =
  \ (@ (a_aKM :: TestCase.Ty)) (ds_dL3 :: TestCase.Expr a_aKM) ->
    case ds_dL3 of _ [Occ=Dead] {
      TestCase.I dt_dLh i_as6 ->
        i_as6
        `cast` (Sub (Sym TestCase.TFCo:R:InterpTyTyInt[0])
                ; (TestCase.InterpTy (Sym dt_dLh))_R
                :: GHC.Types.Int ~# TestCase.InterpTy a_aKM);
      TestCase.B dt_dLc b_as7 ->
        b_as7
        `cast` (Sub (Sym TestCase.TFCo:R:InterpTyTyBool[0])
                ; (TestCase.InterpTy (Sym dt_dLc))_R
                :: GHC.Types.Bool ~# TestCase.InterpTy a_aKM)
    }

Obviously we need to carry around information about what a could be in the specific branch. If I don't indexing over a Datakind and would not use TypeFamilies the cast is a lot easier to understand.

It would be something like this:

Main.eval =
  \ (@ a_a1hg) (ds_d1sQ :: Main.Simpl a_a1hg) ->
    case ds_d1sQ of _ [Occ=Dead] {
      Main.I' dt_d1to i_aFa ->
        i_aFa
        `cast` (Sub (Sym dt_d1to) :: GHC.Integer.Type.Integer ~# a_a1hg);
      Main.B' dt_d1tk b_aFb ->
        b_aFb `cast` (Sub (Sym dt_d1tk) :: GHC.Types.Bool ~# a_a1hg)
    }

This I can understand perfectly well, what troubles me in the TypeFamilies example is this part:

(Sub (Sym TestCase.TFCo:R:InterpTyTyInt[0])
      ; (TestCase.InterpTy (Sym dt_dLh))_R
      :: GHC.Types.Int ~# TestCase.InterpTy a_aKM);

The second line is what really confuses me. What is the semicolon doing there? It seems a bit out of place here or am I missing something? Is there a place where I can read up on this (I gladly take papers if you can recommend one)

Kind regards,

raichoo

The semicolon is syntax for transitivity of coercions.

The latest (as of September 2014) paper about System FC is "Safe Zero-Cost Coercions in Haskell" from ICFP 2014.

In particular, in Figure 3 of that paper we see the syntax of coercions. "γ₁;γ₂" is coercion transitivity. If γ₁ is a coercion that witnesses that "τ₁ ~ τ₂" and γ₂ is a coercion that witnesses that τ₂ ~ τ₃ then "γ₁;γ₂" is a coercion that witnesses τ₁ ~ τ₃.

In the example, when you write eval (I i) = i what the compiler sees on the right hand side is a value of type Int, and what it needs (from the return type of the function) is something of InterpTy a. So now it needs to construct a proof that Int ~ InterpTy a.

Informally, (reading from right to left and ignoring roles - for the details of which see the linked paper):

From doing the GADT pattern match we learn that "a ~ Int" (that's dt_dLh)
So we apply Sym to it, to get "Int ~ a".
Then apply the InterpTy family to get "InterpTy Int ~ InterpTy a" (this is an instance of /congruence/)
Then we compose that transitively with "Sym InterpTyTyInt" (which is the flipped version of the axiom that states that "InterpTy TyInt ~ Int") to get the coercion we're after: "Int ~ InterpTy a"

Recommended topics

Hot tags