On Thu, Apr 2, 2015 at 8:50 AM, Keean Schupke <[email protected]> wrote: > On 2 April 2015 at 12:57, Keean Schupke <[email protected]> wrote: >> Ad-hoc type systems that do not correspond to a sound logic lead to >> trouble in my opinion. > > To compare with Lamba-calculus, every term in lambda calculus is a lambda, > there is nothing else. However, you can represent booleans and integers with > lambda expressions using Church encodings. We can take a short-cut and use > familiar symbols to represent those lambda expressions: > > id = \a . a > > true = \a . \b . a > false = \a . \b . b > > so now we can write: > > id true > > However 'true' is a lambda expression and this is important, because the > laws of lambda calculus (beta reduction etc) are only expressed in terms of > lambdas. Introducing something from outside of lambda calculus (another > operator other than lambda) requires new axioms to be added to the system, > and essentially is not lambda calculus any more and may not share any of the > properties we want from lambda calculus (reduction has a normal form etc). > All these things would need to be re-proved.
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 don't understand where you are coming from sometimes. You seem to take certain famous results very seriously without understanding the nuances of how it all fits together. > The same is true of type theory, the axioms are defined solely types. So if > you introduce something that is not a type, you need to introduce new axioms > to what is now "type+whatever" theory, and re-prove all the important > 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. > So by keeping everything a type, we avoid inventing a new system, and we > keep all the existing proofs. All wee have to do is represent what we want > using types (so the type-level encodings of Peano numbers are the equivalent > of church encodings). > > Fortunately the type level encoding of a Boolean is simple, we need two > types "True" and "False". Do True and False have elements? Interesting ones? How about (fun (x:True)=>x)? What are its elements? What are all these elements doing for you? How does it make the theory any simpler to have to deal with this? I do not doubt the possibility of encoding things with types. I doubt that there's any point. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
