* Martin-Lof type theory gentle introduction please @ 2014-02-03 1:51 Vasili I. Galchin 2014-02-04 4:46 ` Patrik Eklund ` (3 more replies) 0 siblings, 4 replies; 6+ messages in thread From: Vasili I. Galchin @ 2014-02-03 1:51 UTC (permalink / raw) To: Categories mailing list Hello Cat List, I have downloaded many papers about Martin-Lof type theory papers ( .... maybe I just need to pound my head against the wall like other areas that I have I learned until a light goes on my mind?). However, any help on gentle tutorials on this subject would be much appreciated. Kind regards, Vasili [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: Martin-Lof type theory gentle introduction please 2014-02-03 1:51 Martin-Lof type theory gentle introduction please Vasili I. Galchin @ 2014-02-04 4:46 ` Patrik Eklund 2014-02-06 12:49 ` Yoshiki Kinoshita (nifty) ` (2 subsequent siblings) 3 siblings, 0 replies; 6+ messages in thread From: Patrik Eklund @ 2014-02-04 4:46 UTC (permalink / raw) To: categories Hi Vasili, This is not an easy one, since that "theory" has changed form every now and then. I cannot but see it as related to the unsolved issue of the distinction between terms and sentences in logic. When we mix the two, or when we are unclear of the "types" of the two, we will not be able to proceed. Church in 1940 spoke about the 'iota' and 'o' "types of types", where 'iota' is potentially the type of possible sorts in a "conventional signatures". Then 'o' is the "type of propositions", but Church was humble to say that the formal situation about this is not clear. In my view this has not been properly solved since then. See our "Modern eyes on lambda-calculus" under GLIOC (www.glioc.com) for a notion of a three-level signature that may be a solution to some of the problems in this context. Martin-L??f started off with a universes V of types, and added an "axiom" saying "V is also a type", i.e. is part of that V, so "V \in V" was seen to be ok. It turned out not to, so later it was changed by others to "Prop \in Type", where Type is like Church's iota and Prop like Church's o. This still doesn't distinguish between terms and sentences in a proper way, and type constructors kind of come to rescue "from the outside" and are indeed not "internalized" within any signature. Dependent data typing is full of that "externalization". Howards 1969 note (circulated among a few, eventually published upon request by 1980) on the subject is also fine, continuing e.g. what Curry and Fey wrote a decade before, but these notes and writings also do not conclude anything about Church's dilemma about iota and o. Needless to say, Heyting's book is "set-theoretic" so it doesn't help at all. I don't know the "type theory" history and atmosphere from the time of around 1965 (I was seven years old at that time), but I can imagine that there was a bit of "fictive mathematics" and ambitions to establish "new foundations" around tables here and there at that time and during the next decade or even two. Whether this has been useful or harmful for computer science as a whole is difficult to say, but obviously, lots of functional languages have been created upon different views of those "axioms". Many definitely say it has all been very useful, but I have started to have "foundational and constructive doubts", at the age of 55. "Imperative" and "algorithm" is still allowed to be "outside everything", and this privilege is quite "interesting?", but also doubtful. You may want to recall e.g. what Kleene said in his Metamathematics about the "metamathematical proposition" R(x,Y): "There must be a decision procedure or algorithm for the question whether R(x,Y) holds". Indeed there must be. Otherwise G??del's "theorems" are doubtful. Maybe G??del's "theorems" are basically paradoxes, showing how obscure the foundations really are. Freely making propositions related to truth and provability, and feeling privileged not to keep concepts clearly apart from each other, i.e. "mixing bags", leads to many things, but also leads to trouble. Even concerning the distinction between term and sentence, I strongly believe we need to be formal firstly about the term monad (see "Fuzzy terms" under GLIOC), in order to be "constructive" about terms. Thereafter we quickly realize that terms actually reside in sentences. Substitution and compositions with it is for terms, not for sentences. There is a certain "lativity" in all this, and "lativity of choice" if you want to be foundational about it. I don't think there is a "unique" or "canonic" foundations. Basically I am not sure you will find that gentle "tutorial", but if you do, I would also be interested to read it. However, a potpourri tutorial or paper is no good, because the light will just keep staying out, leaving me in the dark, and even worse, in the "foundational gutter". Cheers, Patrik -- Prof. Patrik Eklund Ume?? University Department of Computing Science SE-90187 Ume?? Sweden ------------------------- mobile: +46 70 586 4414 website: www8.cs.umu.se/~peklund Skype: patrikeklund Adobe Connect: https://connect.sunet.se/patrikeklund/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: Martin-Lof type theory gentle introduction please 2014-02-03 1:51 Martin-Lof type theory gentle introduction please Vasili I. Galchin 2014-02-04 4:46 ` Patrik Eklund @ 2014-02-06 12:49 ` Yoshiki Kinoshita (nifty) 2014-02-07 14:34 ` matias 2014-02-11 19:08 ` Urs Schreiber 3 siblings, 0 replies; 6+ messages in thread From: Yoshiki Kinoshita (nifty) @ 2014-02-06 12:49 UTC (permalink / raw) To: Vasili I. Galchin; +Cc: Categories mailing list Your purpose of and approach to learning Martin-Löf type theory is not clear to me, but I would recommend the following lecture note as a generic introduction to everyone who wishes to know something about Martin-Löf type theory: Per Martin-Löf. On the Meanings of the Logical Constants and the Justifications of the Logical Laws. Nordic Journal of Philosophical Logic, 1(1): 11–60, 1996. http://docenti.lett.unisi.it/files/4/1/1/6/martinlof4.pdf Above all, it is written by Martin-Löf himself! Yoshiki. On 2014/02/03, at 10:51, Vasili I. Galchin <vigalchin@gmail.com> wrote: > Hello Cat List, > > I have downloaded many papers about Martin-Lof type theory papers > ( .... maybe I just need to pound my head against the wall like other > areas that I have I learned until a light goes on my mind?). However, > any help on gentle tutorials on this subject would be much > appreciated. > > Kind regards, > > Vasili > > > [For admin and other information see: http://www.mta.ca/~cat-dist/ ] Yoshiki Kinoshita 木下佳樹 [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: Martin-Lof type theory gentle introduction please 2014-02-03 1:51 Martin-Lof type theory gentle introduction please Vasili I. Galchin 2014-02-04 4:46 ` Patrik Eklund 2014-02-06 12:49 ` Yoshiki Kinoshita (nifty) @ 2014-02-07 14:34 ` matias 2014-02-09 18:16 ` Mike Stay 2014-02-11 19:08 ` Urs Schreiber 3 siblings, 1 reply; 6+ messages in thread From: matias @ 2014-02-07 14:34 UTC (permalink / raw) To: Vasili I. Galchin; +Cc: Categories mailing list Almost two decades ago I studied Type Theory in Uruguay on a course organized, if I remember correctly, by Gustavo Betarte and Alvaro Tasistro. In those times we used "Programming in Martin Lof type theory" by Nordstrom. I don't know if this is still considered to be the best introduction. In any case, anyone interested in Type Theory may also be interested in a 2000 document made recently available by Bob Walters in http://rfcwalters.blogspot.com.ar/2013/10/interview-with-bill-lawvere-by-felice.html It contains historical information that I am pretty sure is not available in other sources and that should help any newcomer to understand Type Theory in a broader categorical context. Mat?as Menni. "Vasili I. Galchin" <vigalchin@gmail.com> escribi?: > Hello Cat List, > > I have downloaded many papers about Martin-Lof type theory papers > ( .... maybe I just need to pound my head against the wall like other > areas that I have I learned until a light goes on my mind?). However, > any help on gentle tutorials on this subject would be much > appreciated. > > Kind regards, > > Vasili [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: Martin-Lof type theory gentle introduction please 2014-02-07 14:34 ` matias @ 2014-02-09 18:16 ` Mike Stay 0 siblings, 0 replies; 6+ messages in thread From: Mike Stay @ 2014-02-09 18:16 UTC (permalink / raw) To: matias; +Cc: Vasili I. Galchin, Categories mailing list On Fri, Feb 7, 2014 at 7:34 AM, <matias@lifia.info.unlp.edu.ar> wrote: > Almost two decades ago I studied Type Theory in Uruguay on a course > organized, if I remember correctly, by Gustavo Betarte and Alvaro > Tasistro. In those times we used > > "Programming in Martin Lof type theory" by Nordstrom. That book has been made freely available: http://www.cse.chalmers.se/research/group/logic/book/book.pdf -- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: Martin-Lof type theory gentle introduction please 2014-02-03 1:51 Martin-Lof type theory gentle introduction please Vasili I. Galchin ` (2 preceding siblings ...) 2014-02-07 14:34 ` matias @ 2014-02-11 19:08 ` Urs Schreiber 3 siblings, 0 replies; 6+ messages in thread From: Urs Schreiber @ 2014-02-11 19:08 UTC (permalink / raw) To: Vasili I. Galchin; +Cc: Categories mailing list Hi, the nLab page on type theory has a fairly broad and commented collection of pointers to type theory literature, introductions, textbooks, for logic or computer science, etc. Here: http://ncatlab.org/nlab/show/type+theory#References Personally I would recommend one reference above all others: the introduction chapter to the homotopy type theory book: http://ncatlab.org/nlab/show/Homotopy+Type+Theory+--+Univalent+Foundations+of+Mathematics Best wishes, Urs On 2/3/14, Vasili I. Galchin <vigalchin@gmail.com> wrote: > Hello Cat List, > > I have downloaded many papers about Martin-Lof type theory papers > ( .... maybe I just need to pound my head against the wall like other > areas that I have I learned until a light goes on my mind?). However, > any help on gentle tutorials on this subject would be much > appreciated. > > Kind regards, > > Vasili > > > [For admin and other information see: http://www.mta.ca/~cat-dist/ ] > [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2014-02-11 19:08 UTC | newest] Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2014-02-03 1:51 Martin-Lof type theory gentle introduction please Vasili I. Galchin 2014-02-04 4:46 ` Patrik Eklund 2014-02-06 12:49 ` Yoshiki Kinoshita (nifty) 2014-02-07 14:34 ` matias 2014-02-09 18:16 ` Mike Stay 2014-02-11 19:08 ` Urs Schreiber
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).