On Tue, Jun 9, 2015 at 11:10 AM, Keean Schupke <ke...@fry-it.com> wrote: > On 9 June 2015 at 14:48, Matt Oliveri <atma...@gmail.com> wrote: >> >> It's true that dependent types and refinement types can look very >> similar, but there's a real difference. I can't explain it simply, >> just point out that it causes problems in most forms of dependent type >> theory, but not in Nuprl. Nuprl has an unusual set of deduction rules >> that allow you to use well-typed terms (proofs) to establish that some >> other term (program) has a certain type. It has some other odd stuff >> too. The subtlety is why you truly lose expressiveness without this >> (as a programming language; logics can do without it), and why there's >> no good workaround. > > Yes, I think Nuprl is extensional, but this has other problems.
It's true that Nuprl is extensional, but that's not what I was talking about. Regular extensional type theory (ETT) is essentially the same as intentional type theory (ITT) plus some extensionality principles. Observational type theory (OTT) provides this (and also better computation rules), for example. Translation to ITT or OTT is not the only way to check developments in ETT. There's also a new system called Andromeda, which tries to check ETT more directly. However, I'm worried Andromeda's approach requires too many type annotations internally to be efficient. Plain ETT is kind of a dumb thing from a programming point of view. It says too little about terms to reason about them as flexibly as if you knew they were programs. But it says enough that you lose the good proof theory of ITT. Nuprl is actually easier to deal with than plain ETT, because you don't have to avoid contradicting any of ETT's many categorical models. (Because you've decided it's OK to contradict them.) The problem with non-Nuprl dependent type theory (for programming) is that only Nuprl is specifically about refinement types for programs, that's all. (You could add refinement types to plain ETT, but you'd still have gaps because ETT is not specifically about programs, and checking would be harder, because you cannot implicitly assume terms work like programs.) > HoTT tries to dance the line between intensional and extensional. That's a popular misimpression, I'd say. HoTT needs two notions of equality, one of which is very extensional. ITT provides the necessary distinction with judgmental vs propositional equality. But HoTT doesn't need to be ITT. As long as you have an equality that respects homotopy, and another equality that is respected by the typing judgement (which does not respect homotopy, which is why they have to be different), you're set. Both equalities can be extensional. In other words, the problem with plain ETT (or Nuprl) for HoTT is not that it's extensional, but that it has only one equality. > I don't plan on using dependent types, but instead on lifting values, which > I don't think has these problems. Which problems are you talking about anyway? I see more problems with the lifting values approach, because you don't have enough (any?) type-level computation, which you would need to get sensible equality for sophisticated computations on lifted values. Do you know about SHE, by the way? https://personal.cis.strath.ac.uk/conor.mcbride/pub/she/ This is the kind of hacking around with Haskell's type system that you seem to want. I'd be interested to hear your thoughts on it, if you have any. My impression is that this sort of thing is well known to hit a brick wall beyond toy examples. Dependent typing looks hard because you need to really deal with equality, and many systems cut corners and use an equality that isn't really right, but requires fewer rules, and they run into trouble later. But the Nuprl guys were hacking away, verifying functional programs back in the '80s, and they're still using essentially the same system. Pick the equality with the right semantics and win. _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
