search

Gabriella439 / Haskell-Morte-Library

A bare-bones calculus-of-constructions
BSD 3-Clause "New" or "Revised" License
375 stars 25 forks source link

Why lambda calculus. Why not LISP? #66

Open AnthonyJacob opened 7 years ago

AnthonyJacob commented 7 years ago

Isn't LISP better suited to be functional JSON?

Gabriella439 commented 7 years ago

One of the requirements behind morte is that all expressions can be strongly normalized (even functions), which implies that morte must be a total and typed programming language. I'm not familiar with a total and typed way to implement LISP

VictorTaelin commented 7 years ago

LISP means many things. If you mean something like Common Lisp, Clojure or Scheme, they're nowhere near as simple as Morte, and don't have the same modularity of Morte terms (because of global state and side effects).

@Gabriel439 mind the untyped λLA-calculus and the λEA-calculus are strongly normalizing, and elegantly so (expressing exactly the terms of poly and elementary time complexity, resp.). There are other benefits of a type system, though, they contain precise information on what your term is and what inputs it expects.

For example, when you receive a render : State -> VirtualDOM function on Moon (or Lisp, or whatever), how do you know if it actually implements a State -> VirtualDOM function? There is no way and it could be something completely different.

ChristopherKing42 commented 7 years ago

@Gabriel439 Lisp sort of is a Lambda Calculus. I'm sure there is some way to express the Calculus of Constructions using Lisp syntax (I'm not sure if it would be worth it though).

Also see https://stackoverflow.com/q/3323549/1172541