Martin-Lof type theory gentle introduction please

Martin-Lof type theory gentle introduction please

[Vasili I. Galchin]

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/ ]

Re: Martin-Lof type theory gentle introduction please

[Patrik Eklund]

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/ ]

Re: Martin-Lof type theory gentle introduction please

[Yoshiki Kinoshita (nifty)]

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/ ]

Re: Martin-Lof type theory gentle introduction please

[matias]

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/ ]

Re: Martin-Lof type theory gentle introduction please

[Mike Stay]

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/ ]

Re: Martin-Lof type theory gentle introduction please

[Urs Schreiber]

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/ ]