On 2 April 2015 at 14:25, Matt Oliveri <[email protected]> wrote: > Keean, do you _like_ the untyped lambda calculus? Is it either a > consistent logic or no types at all for you? Did you know untyped > systems can also be presented as typed systems with a single type? If > you do that with the untyped lambda calculus, the corresponding logic > is inconsistent. >
I used lambda calculus as an example, to demonstrate that you need to encode within the system, or else you change the system. If you change the system you need to re-prove the results. > You seem to be under the hilarious misimpression that everything in > MLTT is a type. It ain't so! Ask any proof assistant: "fun (x : 4) => > x" is nonsense. > There is nothing fundamentally wrong with that statement, I could write; fun (x : succ (succ (succ (succ zero)))) => x So I could allow "4" so be a shorthand for succ (succ (succ (succ zero))) and then hide the succ/zero types inside a module. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
