Archive for November, 2010

Size-indexed logical relations

Tuesday, November 30th, 2010 by Nils Anders Danielsson

Previously we have discussed using the partiality monad to define operational semantics for partial languages. Last Friday I talked about how I have used sized types (in MiniAgda) to define a compatible program inequality relation on top of such a semantics. The definition I ended up with turned out to be quite similar to step-indexed logical relations.

Interested readers can have a look at the (very verbose) MiniAgda code.

Modular datatypes and folding for functions

Friday, November 5th, 2010 by Laurence E. Day

Today I presented part of Wouter Swierstra’s “Data types à la carte” (thanks for the correction, French guy!) paper (JFP 2008). To this end, I showed a solution to the expression problem by way of modularising datatypes with coproducts of type constructors and constructing initial algebras for generic functor folds as a supported operation of a type-class, as well as a method for defining ‘smart constructors’. By way of explanation, I defined a function isomorphic to the traditional evaluate function on integers and addition. Discussion then (predictably!) turned towards implementing these ideas in Agda – interest seemed quite high.

data Fix f = In (f (Fix f))
data (f :+: g) e = Inl (f e) | Inr (g e)

fold :: Functor f => (f a -> a) -> Fix f -> a
fold f (In t) = f (fmap (fold f) t)

data Val e = Val Int
data Add e = Add e e
type Expr = Fix (Val :+: Add)

For the class constraint on the fold operation to be satisfied, we need the both the type constructor coproduct and all components to be functors themselves.

instance (Functor f, Functor g) => Functor (f :+: g) where
fmap f (Inl x) = Inl (fmap f x)
fmap g (Inr y) = Inr (fmap g y)

instance Functor Val where
fmap f (Val n) = Val n

instance Functor Add where
fmap f (Add x y) = Add (f x) (f y)

We declare our evaluator algebra as a supported operation of a typeclass defined for an arbitrary functor.

class (Functor f) => Eval f where
  evalAlg :: f Int -> Int

instance (Eval f, Eval g) => Eval (f :+: g) where
  evalAlg (Inl x)  = evalAlg x
  evalAlg (Inr y)  = evalAlg y

instance Eval Val where
  evalAlg (Val n) = n

instance Eval Add where
  evalAlg (Add x y) = x + y

eval               :: (Eval f) => Fix f -> Int
eval               = fold evalAlg

In order to define the smart constructors for manipulating data in this format, we need to define a subtyping relation with (unfortunately) a pair of overlapping instances.

class (Functor sub, Functor sup) => sub :<: sup where
  inj :: sub a -> sup a

instance (Functor f) => (:<:) f f where
  inj = id

instance (Functor f,
          Functor g) => (:<:) f (f :+: g) where
  inj = Inl

instance (Functor f,
          Functor g,
          Functor h,
          (:<:) f g) => (:<:) f (h :+: g) where
  inj = Inr . inj

We're now in a position where we can easily define both a carrier function into a supertype (inject) and smart constructors for our language.

inject      :: (g :<: f) => g (Fix f) -> Fix f
inject      = In . inj

val         :: ((:<:) Val f) => Int -> Fix f
val n       = inject (Val n)

add         :: ((:<:) Add f) => Fix f -> Fix f -> Fix f
n `add` m   = inject (Add n m)

Now we can very easily define instances of the Expr datatype and evaluate them just as we would expect to if our datatype was defined in the standard way:

example :: Expr
example = val 18 `add` val 24

> eval example
> 42

I wish to use the work presented here as part of a framework upon which to construct a compiler fully modular in its source/target languages and the computations it supports.