she's faking it

faking dependent types

Are the terms really breaking through the colon?

Not exactly. What she's doing has rather more of the flavour of Omega, which allows you to declare datakinds — kinds containing type-level data, kept separate from run-time data. She retains the separation of type-level data from run-time data, but saves you the effort of declaring datakinds by recycling your datatypes. Just put a type in {..}, the braces of upward mobility, and it's a kind! Now put expressions built from constructors and variables in {..} to shift them up to the type level.

Here's an example:

data Nat = Z | S Nat
 
data Vec :: {Nat} -> * -> * where
  VNil :: Vec {Z} x
  (:>) :: x -> Vec {n} x -> Vec {S n} x

Now you can write stuff like.

vapp :: Vec {n} (s -> t) -> Vec {n} s -> Vec {n} t
vapp VNil VNil = VNil
vapp (f :> fs) (s :> ss) = f s :> vapp fs ss

type level programs

By a miracle of stunning cheapness, this old pal also goes with the new gal:

type family (m :: {Nat}) :+ (n :: {Nat}) :: {Nat}
type instance {Z} :+ n = n
type instance {S m} :+ n = {S} (m :+ n)
 
vappend :: Vec m x -> Vec n x -> Vec (m :+ n) x
vappend VNil ys = ys
vappend (x :> xs) ys = x :> vappend xs ys

Mark you well that :+ lives in the type language, so it's got to be {S} (m :+ n), not {S (m :+ n)}. The latter would treat :+ as a lifted data constructor.

all fur coat and no knickers

Of course, it's a fiddle. Let's look at what she gives to ghc.

data Nat = Z | S Nat

data Vec :: * -> * -> * where
  VNil :: Vec (SheTyZ) x
  (:>) :: x -> Vec (n) x -> Vec (SheTyS n) x

vapp :: Vec (n) (s -> t) -> Vec (n) s -> Vec (n) t
vapp VNil VNil = VNil
vapp (f :> fs) (s :> ss) = f s :> vapp fs ss

type family (m :: *) :+ (n :: *) :: *
type instance (SheTyZ) :+ n = n
type instance (SheTyS m) :+ n = (SheTyS) (m :+ n)

vappend :: Vec m x -> Vec n x -> Vec (m :+ n) x
vappend VNil ys = ys
vappend (x :> xs) ys = x :> vappend xs ys

data SheTyZ = SheTyZ
data SheTyS x1 = SheTyS x1
data SheTyVNil = SheTyVNil
data (:$#$#$#:>) x1 x2 = (:$#$#$#:>) x1 x2

She erases fancy kinds to *, and translates data constructors to type constructors with ugly names. She also declares type-level versions of your data constructors, with said ugly names. Note, if you want to use infix data constructors, you'll need {-# LANGUAGE TypeOperators #-} to permit the type-level version she generates.

Note that she puts lots of brackets in. Better safe than sorry. Also, you get to write {} for {()} and {x,y} for {(x,y)}, and so on.

lifting standard stuff

You can find ShePrelude with some precooked goodies.

pi kinds

Undertested, but you should be able to write dependent kinds like

pi (x :: *)(n :: {Nat}). {Vec {n} x} -> *

desugaring to * -> * -> * -> *, of course!

gremlins

• You can write type variables in {..} kinds, but explicit forall is not properly implemented yet.
• Try making Vec {n} an Applicative instance and learn something!
• Name mangling is just dumb, so it's easy to engineer clashes.
• Erasure means no nice kind-checking. Edwin says I should transform kind-checking problems into the analogous type-checking problems and fix them up with #line pragmas to boot. Simon says we should just implement it properly in GHC.
• She doesn't lift literals.

a more accurate picture?