monads for lambda calculus
jon.gallagher.04
I have a program that serves a lambda calculus reducer, but I want to
play with it and see what various class representations give, such as
functors and monads.
So consider
> data Lambda a = Var a | Abst a (Lambda a) | Apply (Lambda a) (Lambda a) deriving Eq
Then, of course fold,
> foldLam :: (l -> w) -> (l -> w -> w) -> (w -> w -> w) -> Lambda l -> w
> foldLam var abst app (Var a) = var a
> foldLam var abst app (Abst x m) = abst x (foldLam var abst app m)
> foldLam var abst app (Apply m n) = app (foldLam var abst app m) (foldLam var abst app n)
So that we can give an instance of functor,
>instance Functor Lambda where
> fmap f = foldLam (Var . f) (\x -> Abst (f x)) Apply
Next we can try to write an instance of monads. We have an obvious
"return a = Var a"
And already fmap, so we can do
>instance Monad Lambda where
> return a = Var a
> lam >>= f = joinL (fmap f lam)
> where joinL = foldLam id (\x -> Apply x) Apply
> -- joinL = foldLam id (\x m -> Apply m x) Apply
Yet neither of these really make sense. On one hand it is saying for
an abstraction whose bound variable is a term, apply the variable to
what it binds. The one that makes more sense to me is the second
where the bound variable (a term) is post applied to the term which it
is applied, so that
joinL (\(\x.x).M) = M (\x.x), which will substitute (\x.x) into M
under beta. Yet, it doesn't work like I expected (note** I did not
work out monad laws as of right now, since I wasn't sure if this is
even a good implementation for which to work them out)
Any suggestions?
Thank you,
Dirk Thierbach
> I have a program that serves a lambda calculus reducer, but I want to
> play with it and see what various class representations give, such as
> functors and monads.
> So consider
>> data Lambda a = Var a | Abst a (Lambda a) | Apply (Lambda a) (Lambda a) deriving Eq
BTW, if you define the representation this way, a nice test case is
(\x.x x)(\x.x x). If that doesn't work like it should, you need to improve
the alpha-conversion handling :-)
> Then, of course fold,
>> foldLam :: (l -> w) -> (l -> w -> w) -> (w -> w -> w) -> Lambda l -> w
>> foldLam var abst app (Var a) = var a
>> foldLam var abst app (Abst x m) = abst x (foldLam var abst app m)
>> foldLam var abst app (Apply m n) = app (foldLam var abst app m) (foldLam var abst app n)
>
> So that we can give an instance of functor,
>>instance Functor Lambda where
>> fmap f = foldLam (Var . f) (\x -> Abst (f x)) Apply
BTW, one can define fold and (f)map for every covariant ADT, so that's
in no way special to Lambda. Though I think it's a bit roundabout to
define map in terms of fold.
> Next we can try to write an instance of monads.
Why try for a monad here? If you view an ADT as an F-algebra, fold
and map are straightforward. A monad, OTOH, needs an adjunction,
which is a lot stronger. I can't imagine how a representation of
lambda terms should give rise to an adjunction. You might be able
to squeeze some variant of the other well-known types of monads in,
but that would be somewhat superficial.
>>instance Monad Lambda where
>> return a = Var a
>> lam >>= f = joinL (fmap f lam)
>> where joinL = foldLam id (\x -> Apply x) Apply
>> -- joinL = foldLam id (\x m -> Apply m x) Apply
> Yet neither of these really make sense.
Exactly :-) And using eta-equivalence,
\x -> Apply x === Apply and
\x m -> Apply m x === flip Apply
so you're really just writing "foldLam Apply Apply" resp.
"foldLam (flip Apply) Apply". That looks vaguely like you're trying
to use Abst and Apply like variants of (:). Now that could work out
formally with a bit of tweaking if you're trying to model a variant of
the list monad into Lambda, but since the purpose of the abstraction
in the lambda term is the *binding*, it really doesn't capture the
spirit of a lambda term.
> I did not work out monad laws as of right now, since I wasn't sure
> if this is even a good implementation for which to work them out
I didn't either, but I would expect them to fail.
- Dirk
jon.gallagher.04
data types are there own folds. So that
nil = \nc.n
cons a l = \nc. c a (l n c) <=>
cons = \al.\nc.c a (l n c)
Then
fold v f l = l v f <=>
fold = \vfl.lvf
And
map f l = fold nil (\a m. cons (f a) m) l <=>
map = \f l . fold nil (\am.cons (f a) m) l
The interesting one here is,
var = \a.\v ab ap. v a
abst a m = \lambda v ab ap . ab a (m v ab ap), where we curry it to
get
abst = \am.\v ab ap . ab a (m v ab ap)
apply = \m n.\v ab ap . ap (m v ab ap) (n v ab ap)
And we have
fold varF absF appF term = term varF absF appF (then curry it)
fold = \varF absF appF term . term varF absF appF
... And so on ...
This is very interesting material, I personally wouldn't have guessed
that there is such a simple pattern to defining all inductive data and
their typical functions!
> You might be able
> to squeeze some variant of the other well-known types of monads in,
> but that would be somewhat superficial.
Yes, this is the tree monad in lambda clothing.
The main problem I have is that join doesn't make any sense. Take an
expression that has bound variables, which are themselves expessions,
and this should be rewritten as ?
Originally, application in the lambda calculus is non associative, so
I was wandering if the associative law (for monads) would break if I
wrote a monad for it (mistakenly thinking that all inductive types
form monads). The problem is that A (B C) /=beta= (A B) C, in
general, but says nothing about the associativity of functions that
work on lambda terms. What I ended up with is a function that strips
the bound variables off a term and gives you back an underlying tree
representing the lambda terms. Not at all what I expected. So now,
Haskell 6 , me 0.
How can you prove adjunctions exist on data types?
Dirk Thierbach
> Right, that's the point of data in the lambda calculus. Inductive
> data types are there own folds.
Exactly. Though in don't see what the latter has to do with the former :-)
> This is very interesting material, I personally wouldn't have guessed
> that there is such a simple pattern to defining all inductive data and
> their typical functions!
If you haven't done already, I recommend reading up on F-Algebras.
>> You might be able to squeeze some variant of the other well-known
>> types of monads in, but that would be somewhat superficial.
> Yes, this is the tree monad in lambda clothing.
> The main problem I have is that join doesn't make any sense.
Exactly. It's superficial, it's unnatural, it doesn't fit the intended
use. So why insist on it?
> How can you prove adjunctions exist on data types?
In general, they don't necessarily exist. If you look at it categorically,
when you interpret lambda calculus you need a cartesian closed category,
that indeed involves an adjunction, namely the one given by the currying
and uncurrying Homset-isos. But the monad in Haskell that corresponds to that
adjunction is just the state monad. And all that works on a different
level; it doesn't fit the "lambda term as datatype" approach.
So as I said, I don't see any way to turn it naturally into some monad.
Maybe there is, but may guess is that you won't find any (unless you
supercifially embed a different one).
- Dirk