## 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

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
```example :: Expr example = val 18 `add` val 24```
``` ```
```> eval example > 42```