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)
jon.gallagher.04 <jon.gallagher...@gmail.com> wrote: > 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
Right, that's the point of data in the lambda calculus. Inductive 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?
jon.gallagher.04 <jon.gallagher...@gmail.com> wrote: > 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).
|
