2 ms·
Timely topic, I was asking on a lisp/plt discord if there was a lineage between FP/algebraic types and lisp structural thinking (patterns of nested lists of sym
by agumonkey 4y ago
Timely topic, I was asking on a lisp/plt discord if there was a lineage between FP/algebraic types and lisp structural thinking (patterns of nested lists of symbols representing and/or) with destructuring bind.
I see a big parallel between function to turn params into structs and accessors, both being mirrors of each others (cons/car/cdr as the root example) and the fact that a type definition encodes enough information to generate both at the semantic layer, with pattern matching as sugar.
So if any early LCF team member can shed some light if I'm imagining things or if LCF/ML were a rewrite of older recursive lisp practices into a cleaner formalism, I'd be glad.
ps: the fact that some LCF impl. were done in lisp also reinforces my belief.
- c-cube 4y agoCaml was also initially implemented in LeLisp if I recall correctly. :-). An advantage of ML for theorem proving à la LCF is that you can use the type system to enforce some invariants ; namely you can prevent the user from ever building a value of type `theorem` that is not actually a valid theorem. I don't know how that would work in a dynamic language where you have access to everything.