3 ms·

Maybe a twist on the "why is this useful" question ... Users of lisp often are enthusiastic about the idea that lisp is at its core a minimal wrapper around th

by abeppu 5y ago

Maybe a twist on the "why is this useful" question ... Users of lisp often are enthusiastic about the idea that lisp is at its core a minimal wrapper around the untyped lambda calculus (e.g. plus naming, primitive values and operations, etc). Why do we not generally see languages which are minimal wrappers around these typed lambda calculi? Perhaps intermediate languages are built closely around these formal systems (e.g. I'm aware that Haskell Core is closely based around System FC), but languages which are intended for human authors and readers seem to introduce a lot of extra machinery. Why is that? One guess is that lisps cope with being minimal through use of macros and metaprogramming, it's difficult for a typed language to support that level of metaprogramming while maintaining the various guarantees that one wants from such a system.

Zababa 5y ago
> Why do we not generally see languages which are minimal wrappers around these typed lambda calculi? If you add parametric polymorphism, you're not far from ML, which lives on these days as Standard ML and somewhat through OCaml.
shakna 5y ago
> One guess is that lisps cope with being minimal through use of macros and metaprogramming, it's difficult for a typed language to support that level of metaprogramming while maintaining the various guarantees that one wants from such a system. Difficult, but certainly not impossible [0]. [0] https://cakeml.org/ https://cakeml.org/
somewhereoutth 5y ago
My understanding is that Javascript (for all its woes) is more nearly the untyped lambda calculus. For example, you can do: my_list.map(e=>(a=>some_transform(a)+some_other(a))(sanitize(e))) or otherwise in LC: (map my_list (\e (\a (add (some_transform a) (some_other a))) (sanitize e))) Perhaps much of the power or even the success of javascript is that, in its own way, it brings us closer to the light. It could be, with progressive typing systems (as attempted by TypeScript), with a coherent manner of synthesizing ground types (in the LC itself, subject to a kind of logical 'shield' as we might understand from Arduino), and a sensible conceptual model for dealing with side effects / threading, we could find a pure way of programmatic expression - allowing the model within our minds becomes reified once and for all. Or, it could be that this ideal is unreachable in a fundamental sense.
philzook 5y ago
I'm not so sure most lisps are just a wrapper around untyped lambda calculus. The purely functional bits maybe more or less, but mutation and side effects are an integral part of at least scheme and common lisp.
ukj 5y ago
Your conclusion is spot on. The untyped lambda calculus is inconsistent. If the guarantee you want from your system is consistency then you don’t want the untyped lambda calculus. As software engineers who inherently understand system fragility as being an undesirable property we actually prefer para-consistent systems because they don’t “explode” under contradictions. If the principle of explosion entails fragility; paraconsiatency entails anti-fragility.
- zbyforgotpass 5y ago
  An honest question - what is the problem with inconsistency in using lambda calculus as a programming language and not as foundation of mathematics? """The lambda calculus was introduced by mathematician Alonzo Church in the 1930s as part of an investigation into the foundations of mathematics.[7][a] The original system was shown to be logically inconsistent in 1935 when Stephen Kleene and J. B. Rosser developed the Kleene–Rosser paradox.[8][9]""" https://en.wikipedia.org/wiki/Lambda_calculus#History https://en.wikipedia.org/wiki/Lambda_calculus#History
  - ukj 5y ago
    Practically nothing. By virtue of all programming being resource-bounded computations can be interpreted in Linear logic [1]. Linear logic is paraconsistent [2] not consistent. Untyped Lambda calculus is essentially an assembly language and Assembly languages treat their own code as data [3]. Contradictions arrise when a system can mutate its own state. That is the power and pitfall of reflection [4] [1] https://en.wikipedia.org/wiki/Linear_logic https://en.wikipedia.org/wiki/Linear_logic [2] http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/paraconsistent+logic#linear_logic http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/parac... [3] https://en.wikipedia.org/wiki/Metaprogramming https://en.wikipedia.org/wiki/Metaprogramming [4] https://en.wikipedia.org/wiki/Reflective_programming https://en.wikipedia.org/wiki/Reflective_programming

by abeppu 5y ago

Zababa 5y ago

> Why do we not generally see languages which are minimal wrappers around these typed lambda calculi? If you add parametric polymorphism, you're not far from ML, which lives on these days as Standard ML and somewhat through OCaml.

shakna 5y ago

> One guess is that lisps cope with being minimal through use of macros and metaprogramming, it's difficult for a typed language to support that level of metaprogramming while maintaining the various guarantees that one wants from such a system. Difficult, but certainly not impossible [0]. [0] https://cakeml.org/ https://cakeml.org/

somewhereoutth 5y ago

My understanding is that Javascript (for all its woes) is more nearly the untyped lambda calculus. For example, you can do: my_list.map(e=>(a=>some_transform(a)+some_other(a))(sanitize(e))) or otherwise in LC: (map my_list (\e (\a (add (some_transform a) (some_other a))) (sanitize e))) Perhaps much of the power or even the success of javascript is that, in its own way, it brings us closer to the light. It could be, with progressive typing systems (as attempted by TypeScript), with a coherent manner of synthesizing ground types (in the LC itself, subject to a kind of logical 'shield' as we might understand from Arduino), and a sensible conceptual model for dealing with side effects / threading, we could find a pure way of programmatic expression - allowing the model within our minds becomes reified once and for all. Or, it could be that this ideal is unreachable in a fundamental sense.

philzook 5y ago

I'm not so sure most lisps are just a wrapper around untyped lambda calculus. The purely functional bits maybe more or less, but mutation and side effects are an integral part of at least scheme and common lisp.

ukj 5y ago

Your conclusion is spot on. The untyped lambda calculus is inconsistent. If the guarantee you want from your system is consistency then you don’t want the untyped lambda calculus. As software engineers who inherently understand system fragility as being an undesirable property we actually prefer para-consistent systems because they don’t “explode” under contradictions. If the principle of explosion entails fragility; paraconsiatency entails anti-fragility.

zbyforgotpass 5y ago
An honest question - what is the problem with inconsistency in using lambda calculus as a programming language and not as foundation of mathematics? """The lambda calculus was introduced by mathematician Alonzo Church in the 1930s as part of an investigation into the foundations of mathematics.[7][a] The original system was shown to be logically inconsistent in 1935 when Stephen Kleene and J. B. Rosser developed the Kleene–Rosser paradox.[8][9]""" https://en.wikipedia.org/wiki/Lambda_calculus#History https://en.wikipedia.org/wiki/Lambda_calculus#History
- ukj 5y ago
  Practically nothing. By virtue of all programming being resource-bounded computations can be interpreted in Linear logic [1]. Linear logic is paraconsistent [2] not consistent. Untyped Lambda calculus is essentially an assembly language and Assembly languages treat their own code as data [3]. Contradictions arrise when a system can mutate its own state. That is the power and pitfall of reflection [4] [1] https://en.wikipedia.org/wiki/Linear_logic https://en.wikipedia.org/wiki/Linear_logic [2] http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/paraconsistent+logic#linear_logic http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/parac... [3] https://en.wikipedia.org/wiki/Metaprogramming https://en.wikipedia.org/wiki/Metaprogramming [4] https://en.wikipedia.org/wiki/Reflective_programming https://en.wikipedia.org/wiki/Reflective_programming