Does Haskell have a "de-facto" run-time type?

Question

Here's my dilemma: When Haskell program gets compiled, binary executable machine code is generated that can be executed on a physical CPU. When Haskell program gets interpreted, physical CPU performs operations on data from memory locations. Execution realistically happens in some time period whose length depends on the CPU speed.

Since the data has been put into the memory by a compiler that guarantees that every variable is strongly typed, does this mean that Haskell effectively has a run-time type or not?

Clarification: By "run-time type" I mean: the type (in type-theoretical sense) of a variable at the time when the program is executed on a physical processor reachable/identifiable by the language compiler at language compilation time.

Answer 1

Haskell's language features are designed to support complete type erasure. The idea is that the typing rules guarantee that code which passes type checking has the following two properties¹:

1. A value is of one type is never passed to an function expecting another type
2. A function that claims to handle values in some type will handle any possible value in that type

The 2nd property bears expanding on. Obviously partial functions like fromJust and head do not in fact handle any possible value; they explode At runtime if given the wrong value. But they explode in a "well-defined" way, after checking the assumptions they depend upon. It's not possible to write code that attempts to access substructure in values which may not have that substructure, which might cause segmentation faults or interpret random pieces of memory as if they were a different kind of data.

So after type checking is successful, there's no need to store any type information in the compiled program. I cab just throw the types away. I have already proven that if I generate code which blindly performs operations on data assuming that it is of the required shape that nothing will in fact go wrong.

Example time!

data Foo = Foo Int String
data Bar = Bar Int String

Values of Foo and Bar will probably be represented in memory identically²; once you know all values are type correct, all the information needed to define these values is an Int and a String in each case. If you were to look at a memory dump of a running Haskell program, you would not be able to tell whether a given memory object containing a reference to an Int and a String was a Foo or a Bar (or indeed a (Int, String), or any other single constructor type with two fields that are Int and String respectively).

So no, Haskell types do not exist at runtime, in any form.

---

¹ You can of course break these properties using unsafe features, like unsafeCoerce; I'm talking about "normal" Haskell code here.

2 Or they may not. Haskell-the-language makes no guarantees at all about representation at runtime, and it would be perfectly possible for it to store the fields in a different order, or do something else that could distinguish the two. But I'm going to presume that in the absence of any reason to do otherwise, it treats these two types the same.

Answer 2

Run-time type information is commonly found in OOP languages implementations, which carry a "type tag" with every object. Having such information enables one, for instance, to write code such as

void foo(Object o) {
  if (o instanceof SomeClass) {
     ...
  }
}

which is a form of run-time type checking. The "type tag" often comes for free, since every object needs a pointer to the Virtual Method Table and that alone identifies the run-time type of the object.

In Haskell, though, there is no need for such a tag, or for pointers to VMTs. The language was designed without any kind of instanceof operator so that implementations do not have to provide any type tag at run-time. This also leads to a nicer underlying theory, since we get parametricity guarantees on code, also known as "theorems for free!". For instance the following function

f :: [a] -> [a]
f = .... -- whatever

can not be implemented so that f [1,2] = [2,3]. This is because there is, provably, no way to produce 3 for f. The intuition is that f must produce an a, and it can not check that a=Int at run-time (no type tags), so the output of f can only include elements found in its input. This guarantee comes only from the above typing, without even caring about how f is actually implemented.

If you really want an instanceof equivalent, you can use Typeable for that:

f :: Typeable a => [a] -> [a]
f [] = []
f (x:xs) = case cast x of
           Just (y :: Int) -> [2,3]
           Nothing         -> x:x:xs

This will return [2,3] on all nonempty lists if integers. At run-time, a type tag will be passed so that a=Int can be checked.