The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

 

 

From: <coq-club-request AT inria.fr> on behalf of Xavier Leroy <xavier.leroy AT college-de-france.fr>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Tuesday, 2 April 2019 at 16:20
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Impredicative Set

 

Personally I find the idea of programming languages with "Type:Type" interesting.  There was some work on this topic in the 80's, esp. by Cardelli (http://lucacardelli.name/Papers/TypeType.A4.pdf).  

 

Also somewhat later:

http://www.cs.nott.ac.uk/~psztxa/publ/pisigma-new.pdf

(can’t miss a good opportunity for a plug).

 

Btw, I think a cubical version of PiSigma may be an interesting idea.

 

The usual objection is that typechecking is undecidable.  The party line for typed programming languages is that they should be Turing-complete but have decidable type-checking, or maybe even type inference.  F_omega + general recursion fits this profile.

 

True, but also System U, that is System F with System F for Kinds.

 

Btw, Type Theory is Turing complete – you just have to be explicit when you use the partiality monad.

 

This said, OCaml's type checking is undecidable (at the level of modules), and so is Java's (at the level of generics), so there is also room for type systems with undecidable type-checking.

 

 

 

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.