Emma Tye on Martin-Löf Type Theory

See https://msp.cis.strath.ac.uk/msp101.html I wish I had read this description of it before, because now it makes a heck of a lot more sense! 

The simply-typed lambda calculus (STLC) gives us a nice Curry-Howard correspondence with propositional logic by treating the function arrow of STLC as implication. From this we can compute proofs as programs. But a natural question is then: what about predicate logics instead of propositional? Martin-Löf Type Theory (or Intuitionistic Type Theory) is a type theory based on predicate logic, with type constructions representing existentially quantified variables (Sigma) and universally quantified variables (Pi). We can also construct inductively defined families - W-types - as well-founded trees. Note that Martin-Löf's original paper was inconsistent due to having the type-in-type paradox, and that he later introduced a predicative version with universe hierarchies.

In this introduction, we assume knowledge of the STLC and natural-deduction-style sequents for introduction and elimination rules. We will go over the introduction and elimination of the Sigma-type, Pi-type and W-type, universe hierarchies, and equality reasoning. 

You could put it in the form of a threat: if you don't like this, then take the existential type in System F if you prefer! See Fredrik Nordvall Forsberg on Linear Logic.

It's sentences like that last one that make this book so fucking infuriating. I think it's a reference to the impredicative MLTT, but who knows? 

Subscribe to MSP - Strathclyde.

Here's the next of Steve Awodey's Category Theory for MLTT lectures:

 

See Category Theory May Actually be a Disease.

Subscribe to  p473r.

Comments

Post a Comment

Popular posts from this blog

John Searle's Chinese Room Argument

Image
He's fed up with talking about this. I used to have a copy of the little book he wrote called Minds, Brains & Science. Apparently the AI at Google has read it too and gets it completely: How does stuff like this happen? Most people won't even notice what I'm saying even if I point out that the Google search changed the title. The book was really called Minds, Brains & Science , not Minds, Brains & Programs . (But maybe that was a later edition or something?) I asked Google and it said: John Searle's book Minds, Brains and Science did not become "Minds, Brains & Programs"—rather, they are two separate, distinct works published a few years apart: "Minds, Brains, and Programs" (1980): A landmark academic paper published in the journal Behavioral and Brain Sciences. This is where Searle first introduced his famous Chinese Room Argument to challenge the concept of "strong AI". "Minds, Brains and Science" (1984): A shor...
Read more

Tensor Fields and Simplicial Complexes

Image
Listening to Freya Holmér last night I started to get glimmers of an idea I had long ago about how to represent vector spaces in computational processes using this recursive abstract type :  abstype 'a point = POINT   of {getx :  'a vector,       diff :  'a point -> 'a point,       move :  'a point -> 'a point,       scale : 'a -> 'a point,       proj :  'a point -> 'a} with    fun new i (op +) (op -) (op * ) dot =    let fun self x =  POINT       {getx = x,        move = fn (POINT pr) =>           (self (x + (#getx pr))),        diff = fn (POINT pr) =>          self (x - (#getx pr)),        scale = fn i =>          (self (x * i)),        proj = fn (POINT pr) =>     ...
Read more

FUTO FUBS

Image
I think this is the first time they've actually publicly announced anything about this project. See these posts: Eron Woolf on Why Open Source is Failing Matt Mikhailov and Vincent McKibbon on The Problem with Open Hardware Jason Kridner talking About BeagleBoard.org and Software Development .  See these places:  https://danielc.dev/rk/ https://github.com/petabyt/rk https://github.com/futo-org/ret See also  https://pine64.org/devices/pinebook_pro/ . Subscribe to  FUTO .  See  https://github.com/nir9/low-level-learning-resources/tree/master/setups/debian . Subscribe to  Nir Lichtman .  If you're looking for a cool init process, try  https://ctx.graphics/terminal/ . See  Artful Bytes - When to Use a RTOS  and  How to Create a Successful Open Source Project . 
Read more