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
I didn't either, but I would expect them to fail.
- Dirk
|
