4 ms·

The pedant in me agrees (class-constrained types are not types and therefore not subtypes), but the pragmatist in me still wants to think of class-constrained t

The pedant in me agrees (class-constrained types are not types and therefore not subtypes), but the pragmatist in me still wants to think of class-constrained types as forming a subtyping hierarchy :) even if doing so requires explicit typecasting. Some food for thought: In Mercury, you can combine existential types with typeclasses like so: type foo ---> some [T] (foo(T) => printable(T)). Pedantically, foo is a distinct type from any other. However, any T which is printable is effectively a subtype of foo, since you can use it wherever a foo is expecected, modulo some ugly syntax: ['new foo'(5), 'new foo'("apples"), 'new foo'([1, 2, 3])]: list(foo) I believe you can do something similar in OCaml using module types. (Of course OCaml has true subtyping via polymorphic variants and functional objects.) I am not as familiar with Haskell, so I'm not sure if it supports existential types or not. Dependent languages like Coq go even further -- you can augment types with arbitrary predicates to form "sigma types" which can act as subtypes of one another. You can even write entire programs using sigma types without explicit typecasting. However they remain distinct from true types, and therefore do not provide true subtyping (regardless how well-executed the illusion is).

tikhonj 14y ago
You can do similar existential types in Haskell: {-# LANGUAGE ExistentialQuantification #-} data Foo = forall a. Show a => Foo a [Foo 10, Foo "blarg", Foo (Foo (Foo "str")) However, I think having the extra constructor there is very important. If you were willing to overlook extra syntax and the behavior of the type, then even a normal tagged union starts to look like sub-typing! In fact, in practice, that's exactly what you use where you would use sub-typing in a different language. There are some significant differences, but I'm sure you can see a parallel. There is also an intuitive parallel between existential types and normal tagged unions. The existential type is somewhat like a way to create a tagged union for an unbounded number of types. This naturally means it can't actually be tagged--the tag loses its meaning and you now can't recover the type of the contents--but in practical terms they're similar. As I said, thinking of it like sub-typing is a pretty good intuitive guide (although it might lead you astray sometimes). I was just being pedantic; there's something about formal semantics and type theory that just raises the pedant in me :P.
- colanderman 14y ago
  Thanks for the insights!

tikhonj 14y ago

You can do similar existential types in Haskell: {-# LANGUAGE ExistentialQuantification #-} data Foo = forall a. Show a => Foo a [Foo 10, Foo "blarg", Foo (Foo (Foo "str")) However, I think having the extra constructor there is very important. If you were willing to overlook extra syntax and the behavior of the type, then even a normal tagged union starts to look like sub-typing! In fact, in practice, that's exactly what you use where you would use sub-typing in a different language. There are some significant differences, but I'm sure you can see a parallel. There is also an intuitive parallel between existential types and normal tagged unions. The existential type is somewhat like a way to create a tagged union for an unbounded number of types. This naturally means it can't actually be tagged--the tag loses its meaning and you now can't recover the type of the contents--but in practical terms they're similar. As I said, thinking of it like sub-typing is a pretty good intuitive guide (although it might lead you astray sometimes). I was just being pedantic; there's something about formal semantics and type theory that just raises the pedant in me :P.

colanderman 14y ago
Thanks for the insights!