This post uses “type constructor” when it means “data constructor”. Type constructors make types, while data constructors make (data) values (of a type).

I’m not sure why they’re called data constructors instead of value constructors in Haskell, but I remember being very confused by the “data Foo = Foo Whatever” idiom because the Foo on the left was a type constructor while the Foo on the right was a value constructor.

It would be better to talk about tagged records in place of sum types because you would then immediately understand what the subject is about.

I’m commenting because I think it’s interesting to point out. I plan to write a type system into my language that relies on conversions between types, and on tagged records. It won’t have typecases though, because I thought out that the definition of type ended up being very unstable. Also the type annotations do not really have a reason to feedback into the value space.