Extending nodes in Datatypes à la carte

#1

I’m implementing some stuff using data types à la carte and I’ve gotten stuck at the point where I want to annotate some nodes in the tree.

My starting language is lambda calculus

data Fix f = Fix { unFix :: f (Fix f) }
data f :+: g = ... -- defined in the paper
class (Functor sub, Functor sup) => sub :<: sup where
  inj = ... --defined in the paper

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

data Lambda a = Lam String a
data Var a = Var String
data App a = App a a

-- Smart constructors
lambda :: (Lambda :<: f) => String -> Fix f -> Fix f
lambda name = inject . Lam name

var :: (Var :<: f) => String -> Fix f
var  = Inject . Var

app :: (App :<: f) => Fix f -> Fix f -> Fix f
app l = inject . App l

Then the basic lambda calculus would be represented by

type Expr = Fix (Var :+: Lambda :+: App)

If I would like to extend each expression node with let’s say location then I could just encode that in the fix point. Like so:

data FixT a f = FixT {anno :: a, unFixT :: f (FixT a f)
type FixLoc = FixT (Int,Int)

However, if I would want to annotate the type of the parameter in the lambda expression I run into problems. My idea is the following

data AnnoWith anno f a = AnnoWith {ann :: anno,  unAnnoWith :: f a}

type Expr2 = Fix (Var :+: App :+: AnnoWith Type Lambda)

But then creating the smart constructor for AnnoWith such that I can only annotate lambdas is where I get stuck. Is my representation of the annotation correct? If not, how would I do it?
If it is correct then how would I go about making this work?

Thank you! :slight_smile:

EDIT: Here’s a link to the paper

1 Like
#2

I haven’t read the paper, so take this suggestion with a grain of salt.

data Ann a b = Ann a b

inject2 :: (f :.: g :<: h) => f (g (Fix h)) -> Fix h
inject2 = inject . Compose

alam :: (Ann a :.: Lambda :<: f) => a -> String -> Fix f -> Fix f
alam x s = inject2 . Ann x . Lam s

type Expr = Fix (Var :+: Ann Type :.: Lambda :+: App)

If you don’t already have :.:, it can be defined as

newtype (f :.: g) a = Compose{ runCompose :: f (g a) }

with a higher precedence than the other operators.

#3

I’ll try it out! Thanks

#4

It works! Thanks again!