Skip to content

Instantly share code, notes, and snippets.

@sebastiaanvisser
Created February 20, 2010 22:57
Show Gist options
  • Save sebastiaanvisser/309976 to your computer and use it in GitHub Desktop.
Save sebastiaanvisser/309976 to your computer and use it in GitHub Desktop.
Structural typing braindump.
{-# 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+
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment