Structural typing braindump.

gistfile1.hs

{-# LANGUAGE
    TypeOperators
  , KindSignatures
  , TypeFamilies
  , EmptyDataDecls
  #-}
module StructuralTyping where

-- Type level sum and product that carry around an explicit type environment
-- encoded as a heterogenous list.

infixr 5 :+:
data (a :+: b) env = L (a env) | R (b env)

infixr 6 :*:
data (a :*: b) env = a env :*: b env

-- Type level constant functor.

data K f env = K f

-- Type variable environment.

type Empty = ()

type family Head a :: *
type instance Head (a, b) = a
type family Tail a :: *
type instance Tail (a, b) = b

-- Variable references into the environment. These variables are De Bruijn
-- indices into the type environment.

data VarZ env   = VarZ (Head env)
data VarS v env = VarS (v (Tail env))

-- The fixed point combinator introduces a new type variable into the
-- environment which equals the recursive definition. The previous environment
-- will be kept intact as the tail of the environment.

newtype Fix f v = In { out :: f (Fix f v, v) }

type Tag = Int

---------------------------------------------------------------------------------

-- Regular Haskell append function on lists.

data List a = Nil | Cons a (List a)

append :: List a -> List a -> List a
append xs ys =
  case xs of
    Nil       -> ys
    Cons z zs -> Cons z (append zs ys)

{-
The structural type definition of Haskell lists. In our funVM language this
will probably look something like:

  type ListT = fix (Tag | <Tag, a, 0>)
-}

type ListT a = Fix (K Tag :+: K Tag :*: K a :*: VarZ) Empty

-- Now we can implement the funVM version of the append function on the
-- structural list type. The type is fully inferable by the Haskell type
-- checker.

funVM_append
  :: Fix (K Tag :+: K Tag :*: K b :*: VarZ) Empty
  -> Fix (a     :+: K Tag :*: K b :*: VarZ) Empty
  -> Fix (a     :+: K Tag :*: K b :*: VarZ) Empty
funVM_append xs ys =
  case xs of
    In (L (K 0))                    -> ys
    In (R (K 1 :*: K a :*: VarZ u)) -> In (R (K 1 :*: K a :*: VarZ (funVM_append u ys)))
    _                               -> error "should not happen"

{-
The type above is exactly what we expect, and almost equivalent to:

  ListT a -> ListT a -> ListT a

The only major difference is that the inferred type above is a bit more general
because it is polymorph in the tag of the `ys' list. This is because we never
inspect the tag for this list.

In the funVM language we probably want to write the append function down
something like this:

append
   : fix (Tag | <Tag, b, 0>)
  -> fix (Tag | <Tag, b, 0>)
  -> fix (Tag | <Tag, b, 0>)
append xs ys =
  case xs[0] of
    0 -> ys
    1 -> [1, xs[1], append xs[2] ys]

Is it even possible to convert/normalize the type to the following?

append
   : <<Tag, b>*, Tag>
  -> <<Tag, b>*, Tag>
  -> <<Tag, b>*, Tag>

This allows for some weird optimizations:

appendString
   : <<Tag1, Char31>*, Tag1>
  -> <<Tag1, Char31>*, Tag1>
  -> <<Tag1, Char31>*, Tag1>

appendString : Word32+ -> Word32+ -> Word32+

-}