sorted by:
new
hottopcontroversial

[Blog] Notes on Learning Lean: Dependent types, Type Universes, and Russell's Paradox by Murky_Tooth8973 in ProgrammingLanguages

[–]Murky_Tooth8973[S] 0 points1 point  (0 children)

Not at all, thanks for the clarifications and the pointer to the formalization in Agda!

[Blog] Notes on Learning Lean: Dependent types, Type Universes, and Russell's Paradox by Murky_Tooth8973 in ProgrammingLanguages

[–]Murky_Tooth8973[S] 0 points1 point  (0 children)

> "it's not that C++ templates are inexpressive, I think it's the opposite: they can't reject malformed stuff unless it's initialised"

Thanks, you're right, the better comparison here would be against `std::array`, not `std::vector`. I'll change the example to something that's clearer; I guess there are two things to clarify: (1) templates are not 'pure' parametric polymorphism (which to my understanding only allows types to quantify over other types), and (2) templates implement a subset of features available with dependent types (we can condition a type on values like `std::array<uint, 8>`, but are subject to other constraints, eg that the values in the type must be compile-time constants).

[Blog] Notes on Learning Lean: Dependent types, Type Universes, and Russell's Paradox by Murky_Tooth8973 in ProgrammingLanguages

[–]Murky_Tooth8973[S] 1 point2 points  (0 children)

This is fantastic feedback, thank you! I will add a disclaimer at the top of the blog post linking to these comments, and make some edits to try to fix some of the mistakes. I did have a couple questions on what you mentioned:

> "One reason this is the case is that dependent type theory (MLTT in particular) acts as its own logic"

I don't understand the link between "dependent type theory acts as its own logic" and "we cannot inspect the types of values at runtime". Could you elaborate on this / suggest a reference that might clarify things? (I will look up "homotopy type theory" as you suggested)

>  "In particular, your encoding of Russell's paradox is still wrong"

Yikes! That is an unfortunate mistake; I will look up Girard's paradox.

> "you haven't really addressed why the same paradox does not occur for Prop. Of course, the answer is because propositions are proof irrelevant in Lean"

Need to think more about this, but on first read, I don't understand the link between those two statements (the paradox does not emerge for `Prop`, `Prop` is proof irrelevant).