monads for lambda calculus - comp.lang.haskell

Допис з розмови monads for lambda calculus

Dirk Thierbach

Переглянути профіль

Більше налаштувань 21 Жов 2009, 00:59

Групи новин: comp.lang.haskell

Від: Dirk Thierbach <dthierb...@usenet.arcornews.de>

Дата: Tue, 20 Oct 2009 23:59:40 +0200

Місцевий час: Ср 21 Жов 2009 00:59

Тема: Re: monads for lambda calculus

  Переслати | Друк | Дивитися гілку
  | Показати оригінал
  | Повідомити адміністраторів про це повідомлення | Знайти повідомлення від цього автора
  

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

Переслати