3 ms·

The author writes about “path-dependent types”, but all I can see is plain existentials.

• lmm 11y ago
  a1.B and a2.B in the example are path-dependent types - you couldn't express them as just existentials (you could express the types of a1 and a2 as existentials, but you couldn't write "a1.b = Some(b1)" in a purely existential typing system - you need some way to "get the type out").
  • catnaroek 11y ago
    Not with Haskell-style (or, rather, System F-omega-style) existentials, sure. But why not with strong existentials, like what you get with first-class modules in OCaml or 1ML?
    • lmm 11y ago
      At that point this is just semantics. I find the phrase "path-dependent types" useful and intuitive (though admittedly easily confused with "dependent types"); maybe we could use that phrase to describe what OCaml has too?