*finally-tagless*(typed) representations and made an attempt to model the (implicitly typed) lambda calculus. However, I wanted to use the

*parametric higher-order abstract syntax*(PHOAS) technique to obtain variable bindings that are automatically well-scoped.

I arrived at this formulation:

```
class LC rep where
```

var :: p → rep

lam :: (forall p . p → rep) → rep

(I am ignoring applications as they are not important for making my point.)

As Andres Löh has pointed out to me this is not the final-tagless formulation of the regular PHOAS form, as that would add the

`p`

type variable as the second class parameter and the rank-2 `forall`

would appear from "outside".But I liked my simple formulation and the obviously and explicitly parametric lambda body. So I started implementing a rudimentary visualisation instance given a name supply:

```
instance LC ([String] → String) where
```

var = ??? -- const "VAR"

lam f = \supply → ...

It turns out that implementing

`var`

is only possible by giving a constant result, and for `lam`

I am in trouble, because I cannot call `f`

as it expects a polymorphic argument. Both problems are due to the fact that `p`

is too polymorphic. Can we have it a bit less polymorphic in order to make some progress?Thinking about it I came up with the idea of giving each instance a way to constrain the

`p`

variable as it fits. So I changed `class LC`

such:```
class LC rep where
```

type Restricted rep p :: Constraint

var :: Restricted rep p ⇒ p → rep

lam :: (forall p . Restricted rep p ⇒ p → rep) → rep

Now my instance can pick the restriction as it fits:

```
instance LC ([String] → String) where
```

type Restricted ([String] → String) p = ([String] → String) ~ p

var = id

lam f = \supply → ...

As you see I chose the restriction to be

*type equality*which essentially cancels parametricity in this instance and gives me simple HOAS. Filling in

`p`

becomes easy now.```
lam f = \(n:ns) → "\\" ++ n ++ "." ++ (f $ const n) ns
```

Let's try it out! But in order to do that we need an instance of

`Show`

for name supplies. This could be one:

instance Show ([String] → String) where

show f = f $ map (('v':) . show) [0..]

Now we can interpret a lambda term as a name supply.

*Main› lam (\x → lam $ \y → var x) :: [String] → String

\v0.\v1.v0

It works™ :-)

But I can go further. After implementing several other instances I observed that I always wanted to destroy parametricity completely and implement

`var`

as the identity. So why not have these as defaults and reduce the boilerplate by a nice margin? Here is the final class definition that I arrived at:```
class LC rep where
```

type Restricted rep p :: Constraint

type Restricted rep p = rep ~ p

var :: Restricted rep p ⇒ p → rep

default var :: rep ~ p ⇒ p → rep

var = id

lam :: (forall p . Restricted rep p ⇒ p → rep) → rep

I like it so far.

PS: Here are the prerequisites if you want to compile the above yourself:

{-# LANGUAGE UnicodeSyntax, ConstraintKinds, TypeFamilies, RankNTypes, FlexibleInstances, DefaultSignatures #-}

import GHC.Exts

## No comments:

Post a Comment