Thursday, May 3, 2012

Almost LF in Haskell

NOTE:  If this seems a little abstract and useless, you can think of it as a cleaner, more first class version of template Haskell.  I do plan on eventually constructing a library with template Haskell to automatically convert GADT declarations like these into  meta programming dependent types as shown here.

    A while back I had written a post about logic programming using Haskell typeclasses.  The example I had given was fairly minimal, and didn't show the full power of logical programming.  I wanted to show how type inference in combination with logical programming could be used to do meta-programming and program transformations.
    I thus set out to show that lambda calculus could be embedded entirely within the type system using logical programming.  My goal was to have lambda expressions in the type system evaluate to terms which were then converted to runtime values.  This is what I came up with:


1
2
3
4
5
6
7
{-# LANGUAGE
 TypeOperators
 #-}
infixr 0 :$
type m :$ a = m a

infer_explicit = val :: (Step (App (Lam :$ Var Z) :$ Var :$ S :$ S Z) b => Term b)

When compiled, Haskell infers the following type:

1
infer_explicit :: Term (Var (S (S Z)))

However, alone this wasn't good enough.  It is very easy to write incorrect logical code, given how many arguments logical predicates can have.  Type checking makes logical programming that much easier.  However, we are already in working Haskell's type system, so there really isn't a well developed next level.  Haskell does have kinds however, and kinds do support checking if a logical variable is a * or a * -> * ...  This means that at least some amount of checking is being performed.  The next step is figuring out how to name *. It is known that many logic systems can embed a type system for themselves within themselves.  Examine the following example of predicate for testing whether it's argument is a logical number:

1
2
3
4
5
6
data Z
data S a

class Nat a
instance Nat Z
instance Nat a => Nat (S a)

Clearly this code would break if anybody were to add another instance of Nat somewhere else.  So type checking logical code in Haskell can't be done simply with predicates, there needs to be some way to ensure that the instances for a type predicate only correspond to those values that are part of a type.  Haskell already has a something thing that behaves like type:  a type.   So to solve this, we need to connect a single type with type constructors to multiple phantom types.  Instead of the type predicate being a class which determines if it's argument is of that type, we can use Haskell's internal definition of type, and GADTs:

1
2
3
4
5
6
data Nat b where
  Z :: Nat Z
  S :: Nat a -> Nat (S a)

data Z
data S a

Now that we have constructed the predicate on the value level in Haskell, we want to leverage "Nat b" to a predicate.  The way to do this is with another predicate.  "Nat" is a type function, and "Z" and "S a" are both type values.  So we need a predicate which ensures that "Nat"'s arguments are only the type values "Z" and "S a" where "Z" are type the only values usable.  The way to do this is with a class that ensures an Isomorphism between the values that inhabit either these types:

{-# LANGUAGE
 MultiParamTypeClasses,
 GADTs,
 FlexibleContexts,
 StandaloneDeriving,
 FlexibleInstances,
 UndecidableInstances
 #-}
module Nat (Iso(), Nat(..), S(), Z()) where
-- AXIOM: into . outof == id
class Iso m a | a -> m where
  into :: a -> m a 
  outof :: m a -> a

data Nat b where
  Z :: Nat Z
  S :: Iso Nat a => Nat a -> Nat (S a)

data Z where Z' :: Z
data S a where S' :: Iso Nat a => a -> S a
               
instance Iso Nat Z where
  into Z' = Z
  outof Z = Z'

instance Iso Nat a => Iso Nat (S a) where
  into (S' a) = S (into a)
  outof (S a) = S' (outof a)

Notice now that the types S and Z have been given values to make this work.   Also notice that we do not export the values of S' and Z'.  Now when "Iso Nat a" is used as a predicate outside this module, it is guaranteed that "a" will be either "Z" or "S b" where b has the same predicate.

The code from these examples EDIT: Apparently in GHC-7.4 and up, you can define kinds in the language:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
{-# LANGUAGE                                                                                           
 TypeFamilies,                                                                                         
 DataKinds,                                                                                            
 PolyKinds                                                                                             
 #-}
module Kinds where


data N = Z | S N

data family NatFam (a :: N)
data instance NatFam Z
data instance NatFam (S a)

class NatClass (a :: N)
instance NatClass Z
instance NatClass a => NatClass (S a)