Object and Meta, Typefully

In my previous post on constraint programming, I took the following term type as an object language and started doing meta-level work with it:

data Term = Term !Label ![Term]

I handled the meta level in a manner that isn’t particularly typeful:

data Term = Term !Label ![Term] | Metavar Integer

That’s okay for a quick and dirty solver, but there are better options if you want a bit more safety!

quick note: I leave the !s out in all these representations because the one in ![Term] doesn’t actually do that much good (it only achieves head-strictness) so I figured it’s easier to stick to the fast and loose approach

Just use two types

data ObjectTerm = ObjectTerm Label [ObjectTerm]
data MetaTerm = MetaTerm Label [MetaTerm] | Metavar Integer

liftToMeta :: ObjectTerm -> MetaTerm
liftToMeta (ObjectTerm l cs) = MetaTerm l (map liftToMeta cs)

concretise :: MetaTerm -> Maybe ObjectTerm
concretise (MetaTerm l cs) = return . ObjectTerm l =<< mapM concretise cs
concretise Metavar{} = Nothing

This one’s obvious enough. Given only Haskell 2010 type classes to abstract across the equivalents of the Term constructor this can be rather painful to work with because your polymorphic constructor is no good for pattern matching. With view patterns or the upcoming pattern synonyms things become more comfortable though.

data TermView children = Term Label [children] | NotTerm

class Term t where
  term :: Label -> [t] -> t
  matchTerm :: t -> TermView t

instance Term ObjectTerm where
  term = ObjectTerm
  matchTerm (ObjectTerm l cs) = Term l cs

instance Term MetaTerm where
  term = MetaTerm
  matchTerm (MetaTerm l cs) = Term l cs
  matchTerm _ = NotTerm

add :: (Term l, Term r) => l -> r -> r
add (matchTerm -> Term "Z" []) r = r
add (matchTerm -> Term "S" [n]) r = term "S" $ [add n r]

This example only uses view patterns, but pattern synonyms would allow patterns that’re indistinguishable from ordinary ones. Note the type of add though (equivalent to the inferred one) – it can lead to unexpected annotation requirements.

GADTs

One of the great things about GADTs is that you can use phantom types to mark out what might otherwise be subtypes of the GADT – and pattern-matching to perform the equivalent of a safe cast. The bad news is that they don’t play quite so nicely with the rose tree representation: you can’t prove anything without a separate leaf constructor, which makes a bit of a mess of the original code.

data Concrete
data Meta
data Term a where
  Leaf :: Label -> Term a
  Branch :: Label -> [Term a] -> Term a
  Metavar :: Integer -> Term Meta

concretise :: Term a -> Maybe (Term Concrete)
concretise (Leaf l) = return $ Leaf l
concretise (Branch l cs) = return . Branch l =<< mapM concretise cs
concretise Metavar{} = Nothing

The concretise function attempts to prove that a Term can be Concrete via pattern-matching – Metavar is always Term Meta, which effectively taints the entire term it appears in. The concretise function still ends up rebuilding all the Branch nodes though.

An alternative type for concretise is Term a -> Maybe (Term b), and if we’re comfortable with rank-n types we can use (forall a. Term a) as an equivalent to Term Concrete that’s readily usable as Term Meta as well. This means we already get liftToMeta for free if we keep types polymorphic until we care, but failing that it’s just a tree traversal rebuilding the same term at a different type.

Quick and Dirty Optimisation

The version of concretise above rebuilds an entire term just to change its type, but GHC already has the same underlying representations for them. I don’t know a good way of carrying coercions to Concrete or a type variable around, but we do know something the compiler doesn’t – and this means we can cheat.

import Unsafe.Coerce

concretise :: Term a -> Maybe (Term Concrete)
concretise l@Leaf{} = return $ unsafeCoerce l
concretise b@(Branch l cs) = return $ unsafeCoerce b =<< mapM_ concretise cs
concretise Metavar{} = Nothing

Two level types

There’s an alternative approach using two mutually recursive datatypes, which when generalised are parametric in each other. One type handles the per-node structure of a term, while the other handles the recursive structure – and via polymorphism, any additional structure that doesn’t belong to object terms.

data Term wrapper = Term Label [wrapper]

newtype Fix a = Fix { unfix :: (a (Fix a)) }
data Meta object = O (object (Meta object)) | Metavar Integer

liftToMeta :: Fix Term -> Meta Term
liftToMeta (Fix (Term l cs)) = O $ Term l (map liftToMeta cs) 

concretise :: Meta Term -> Maybe (Fix Term)
concretise (O (Term l cs)) = return . Fix . Term l =<< mapM concretise cs
concretise Metavar{} = Nothing

Fix is a type-level fixpoint operator – so it provides recursive structure in types polymorphic in their own children, and nothing else. The O constructor in Meta has much the same structure, but Meta also handles metavariables. As Fix and Meta have completely different internal representations, liftToMeta and concretise both require rebuilding the entire term again.

This approach has the major advantage that it starts to enable a degree of generic programming – we can reuse Fix and Meta for a variety of different object node types. The classic example is Tim Sheard‘s functional pearl on generic unification, which is implemented in the unification-fd package.

It may also be appropriate to use type classes etc much as in the initial example – possibly using one class generalising Term and a second one generalising Fix and Meta, such that an application of the Fix/Meta generalisation is also a generalisation of Term. I haven’t tried it so far though, and it’s possible that the increased annotation burden isn’t worth it.

Chaining Types and the Expression Problem

Having gone as far as two level types, we can try a refactoring:

data ObjectTermNode fix = Term Label [fix]
data MetaTermNode chain fix = O (chain fix) | Metavar Integer

newtype Fix a = Fix { unfix :: (a (Fix a)) }

type ObjectTerm = Fix ObjectTermNode
type MetaTerm = Fix (MetaTermNode ObjectTermNode)

Now the node info for metaterms is also separated from the recursive structure. This generalises to as many different node types as we like, though the collection of constructors used to pass up the chain will grow – clearly this cries out for a type class to match each node type. I’m hoping that with ConstraintKinds someone’ll figure out a good way to write instances that generate the chaining behaviour with only a linear instance count too, but as I’m sticking with the Haskell Platform at present I’m not able to have a go myself yet.

This solution has the advantange of generalising to the Expression Problem: we can add new node types (with corresponding type classes) and new functions reasonably orthogonally. Similarly, other solutions to the Expression Problem are solutions to the problem discussed in this post.

Advertisements

4 thoughts on “Object and Meta, Typefully

  1. Pingback: Introduction to Constraint Programming | flippac

    • Sadly not (I’d have to pay to use cutstom non-inline CSS at present, though I might think about that as the blog grows). I can though – I’d prefer to find a highlight for constructors still, but I can set it to the default grey for now if I don’t figure anything else out, so I’ll get on that while I experiment further/wait for feedback. Is the magenta for literals a problem too?

  2. Pingback: The Simply-typed Lambda Calculus with Constraints | flippac

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s