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 metaprogramming 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:
{# 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:
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:
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:
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 GHC7.4 and up, you can define kinds in the language:
Do userdefined kinds (in recent GHC versions) make this workaround obsolete?
ReplyDeleteLink? Unless they allow for an unbounded hierarchy of types, kinds, sorts, etc and logic programming or type functions on every level of this system then no.
ReplyDeleteThe main point here is that this shows that types can have real kinds, definable at the same level we are defining types. Given a set of types (data S, data Z), a type with values inhabiting it equivalent to the set of types (data Nat a where) by way of isomorphism can also be supplied. This means that the type's kinds are defined as types.
If you mean this, then yes: http://www.haskell.org/ghc/docs/latest/html/users_guide/kindpolymorphismandpromotion.html
ReplyDeleteI'm kinda sad. I was looking forward to writing up my workaround solution using template Haskell.