[vutekst]

> Even in Haskell values must be tagged with types, and the type tags are inspected at runtime.

This does not fit my understanding of pattern matching in Haskell. Say you are matching over a value of type `Maybe String`. The type of the value is always `Maybe String`, it's just that its value might be `Just "foo"` or `Nothing :: Maybe String`. It is not to my knowledge tagged with type information at runtime in a compiled program, merely value information. The different values an ADT disjunction can take on all have the same type as each other.

> Otherwise, pattern matching wouldn't work (pattern matching is always based on type reflection).

What about pattern matching a String against a series of literal values? I don't see how this is based on type reflection, merely inspection of values.

[tel]

In this context "tag" refers to the part of a value of type Maybe a which indicates whether that actual value is of the form Just a or Nothing. In other words, it's entirely runtime information distinguishing between various members of the same type

[vutekst]

This is my understanding as well, and that's why I objected to the parent post's assertion that "even in Haskell values must be tagged with types, and the type tags are inspected at runtime". The enum/ADT discriminator tag is value information rather than type information.

[pron]

Just and Nothing are different types even if the Haskell nomenclature doesn't call them so. The word "type" in Haskell means something different than it does in other languages. Haskell uses type to mean the mathematical notion of a set, while in CS, type usually refers to data memory layout. When comparing Haskell to other languages, we can't confuse terminology. In OO terms, for example, Just and Nothing are subtypes of Maybe, so the tag differentiating the two is exactly the same as that used to verify downcasts from the supertype Maybe to its subtypes, in, say, C++ or Java. Haskell implements the very same mechanism (call it reflection or RTTI).

[tel]

Meh, that's a way to talk about it but the standard type system of Haskell doesn't include subtyping like that. It's possibly you could apply a subtyping analysis to Haskell, but it's certainly non-standard and I'm not sure what you really, literally gain.

[pron]

Haskell doesn't call them subtypes, but they're implemented using type tags, just like RTTI. Haskell simply uses different words to mean the same thing (and the same words to mean different things). You can't say these aren't type tags just because Haskell doesn't call these things types.

[tel]

I can say it's not a subtyping relationship because it happens entirely at runtime and my definition of types—the one consistent with what I referred to as Haskell's standard type analysis—does not include runtime dynamics.

If you want to pick a definition of typing which includes runtime information (and referencing RTTI, clearly you do) then we can shift to that vocabulary and talk about whether such an analysis includes a subtyping judgement. I'm not familiar with it.

But it's certainly not consistent with the standard Haskell type analysis. So there shouldn't be any surprise that the vocab doesn't match up.