Re: Lambda over types.
anatoli wrote: > This is all, of course, of purely academical interest. The notation > is extremely inconvenient to do any real work. I'd rather prefer > a real, language-supported lambda over types. > Or... wait a minute! You did find all those problems; does it mean > you tried to *use* this stuff for something? Just curious. I must start with a profuse apology, because what follows is perhaps of little relevance to the list. I also propose to re-direct the follow-ups to the Haskell Cafe. I have examined your code and then tried a few examples, some of which from my code's regression tests. I have implemented a compile-time lambda-calculator, in a different language. I should say, in a meta-language. The output of the evaluator is a term that can then be compiled and evaluated. The lambda-calculator acts as a partial evaluator. The calculator normalizes a term in a pure untyped lambda calculus. The result is compiled and evaluated in a call-by-value lambda-calculus with constants. Haskell typechecker (augmented with multi-parameter classes with functional dependencies and let on loose) may do something similar. BTW, the meta-language lambda-evaluator code (with the regression tests) can be found at http://pobox.com/~oleg/ftp/Computation/rewriting-rule-lambda.txt The calculator is implemented in CPS, in some sort of extended lambda calculus. Therefore, the code has three kinds of lambdas: of the source language, of the transformer meta-language, and of the target language. The first and the third lambdas are spelled the same and are the same. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Lambda over types.
[EMAIL PROTECTED] wrote (in part): > > anatoli wrote: > > Attached are two interpreters: one for untyped lambda calculus, > > I'm afraid the attached interpreter can't be an implementation of the > lambda calculus. Indeed, it isn't. My bad; I shouldn't have to rely on my failing memory. I believe that all problems you mention are fixable. I will attempt to fix them as time permits. I've already found that I practically have to use de Brujin notation to do substitutions correctly. This is all, of course, of purely academical interest. The notation is extremely inconvenient to do any real work. I'd rather prefer a real, language-supported lambda over types. Or... wait a minute! You did find all those problems; does it mean you tried to *use* this stuff for something? Just curious. -- anatoli tubman __ Do You Yahoo!? Yahoo! Greetings - send holiday greetings for Easter, Passover http://greetings.yahoo.com/ ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Lambda over types.
anatoli wrote: > Attached are two interpreters: one for untyped lambda calculus, I'm afraid the attached interpreter can't be an implementation of the lambda calculus. For one thing, it lacks the hygiene of substitutions: Lambda> :t lambdaEval (A (L X (L Y (A X Y))) T) lambdaEval (A (L X (L Y (A X Y))) T) :: L Y (A T Y) That's OK. However, Lambda> :t lambdaEval (A (L X (L Y (A X Y))) Y) lambdaEval (A (L X (L Y (A X Y))) Y) :: L Y (A Y Y) That is wrong! The correct answer is: L Yfresh (A Y Yfresh) The interpreter in question doesn't appear to be able to manufacture fresh identifiers (i.e., fresh types). Without an ability to expand the set of available identifiers, the capture-free substitution is impossible. Furthermore, some terms fail to evaluate: Lambda> :t lambdaEval (A (L X (A X X)) T) lambdaEval (A (L X (A X X)) T) :: Eval (A (L X (A X X)) T) a => a Lambda> :t lambdaEval (A (A (L X X) T) Y) lambdaEval (A (A (L X X) T) Y) :: Eval (A (A (L X X) T) Y) a => a which is not the result one would've expected. Finally, the interpreter doesn't actually find the normal form. The rule > instance Eval (L v e) (L v e) prevents any reductions under lambda. True, call-by-name or call-by-value interpreters stop short of reducing the body of a lambda form. Normal or applicative order interpreters however -- in order to find the beta-eta-normal form -- should seek and attempt any reduction. The hygienic substitution (with alpha-conversion if necessary) and the repeated identification of the leftmost outermost redex are actually quite challenging. We can guarantee the hygienic substitution if we implement the de Bruijin notation for lambda terms. Another, related technique is coloring of existing identifiers. A macro-expander of R5RS Scheme macros implements the coloring to ensure the hygiene of macro expansions. The macro-expander can be cajoled into painting identifiers on our demand, which has been used in a macro-expand-time lambda calculator. In Haskell, we have to paint manually. A variable in a typechecker-time lambda-calculator has to be represented by a type like Vr (Succ (Succ (Succ Zero))) X. The latter component is the "name" and the former is the color. The Eval and Subst relations should be extended with color_in and color_out type parameters (perhaps with a dependency: term color_in -> color_out). The only non-trivial use of colors is in doing a substitution (L var body)[exp/var']. The bound variable has to be repainted before the substitution in the body. The beta-substitutor itself can do the repainting. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Lambda over types.
anatoli <[EMAIL PROTECTED]> writes: > ghc -fglasgow-exts -fallow-undecidable-instances allows > constructs which amount to lambda abstraction over types. > I've written a small untyped lambda calculus interpreter > in the Haskell class/instance sublanguage, just to prove > this point. (The terms are Haskell *types*.) Cool! Some time ago I wrote a Turing machine evaluator in Haskell types with undecidable instances. It's described at http://www.chttp://www.cl.cam.ac.uk/~kw217/research/misc/undec.html Enjoy! --KW 8-) -- Keith Wansbrough <[EMAIL PROTECTED]> http://www.cl.cam.ac.uk/users/kw217/ University of Cambridge Computer Laboratory. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Lambda over types.
Hal Daume III <[EMAIL PROTECTED]> wrote: > I'd be interested in seeing how you do this. I attempted such a thing a > while back but was unsuccessful. Attached are two interpreters: one for untyped lambda calculus, and one for an Unlambda-style language (combinators). Of course pure lambda terms are not very useful Haskell types. You may use your own types as primitive terms by defining instances of Subst and/or Eval of them. -- anatoli __ Do You Yahoo!? Yahoo! Movies - coverage of the 74th Academy Awards® http://movies.yahoo.com/ lambda.lhs Description: lambda.lhs unlambda.lhs Description: unlambda.lhs
