val singleton

Regardez:

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

Now you can write stuff like.

vec :: forall x. pi (n :: Nat). x -> Vec {n} x
vec {Z} x = VNil
vec {S n} x = x :> vec {n} x

Mumsie! Have the terms broken through the colon? Of course not. ‘pi (n :: Nat).’ is short for ‘forall n. SheSingleton Nat n ->’, which computes by tactical grace to ‘forall n. SheSingNat n ->’, where ‘SheSingNat’ is a GADT with ‘SheWitZ :: SheSingNat {Z}’ and ‘SheWitS :: pi (n :: Nat). SheSingNat {S n}’. Phew! The braces in terms turn ordinary constructors into their SheWitty versions, demanding the corresponding values at the type level.

This is an annoying hack: SheSingleton is a type family, when it would be nicer to make it a data family defined GADT-style: this slicker coding already works in 6.11, but not in 6.10.

type constraints and witnesses

With more heaving and groaning, you can write class constraints {:tm :: ty:}. These are a wart, caused by the way we don't really have properly kinded type-level data. If you know such a thing, you may find it useful to write {:tm :: ty:}, which should give you an witness in (SheSingleton ty tm). Of course, there's a typeclass (SheChecks ty tm) with a method which computes the witness, given a proxy. The above GADT-family translation removes the need for proxies.

This will let us write

instance {:n :: Nat} => Applicative (Vec {n}) where
  pure = vec {:n :: Nat:}
  (<*>) = vapp

gremlins

  • Because pi desugars as forall, if you use pi, you'd better put all the foralls in for everything else.
  • Still undertested, deriving SheSingleton only kicks in for GADT-style datatypes with prefix constructors. More work needed.
  • More namespace landgrabs.
  • You need a ton of LANGUAGE extensions: find out what they are from GHC.
  • Lots of standard stuff still needs singleton instances.
  • I couldn't get vtake to work:
    vtake :: forall x n. pi (m :: Nat). Vec ({m} :+ {n}) x -> Vec {m} x
    vtake {Z} xs = VNil
    vtake {S m} (x :> xs) = x :> vtake {m} xs