## Type-Safe Casts

In a language with non-parametric or ad-hoc polymorphism,
it is possible to determine the identity of a type variable at
run time. With this facility, we can write a function to convert
a term from one abstract type to another, if the two
hidden types are identical. However, the naive implementation
of this function requires that the term be destructed and
rebuilt. In this paper, we show how to eliminate this overhead
using higher-order type abstraction. We demonstrate
this solution in two frameworks for ad-hoc polymorphism:
intensional type analysis and type classes.

This is a Functional Pearl, which was recommended in a previous discussion here.

So I'm looking at the pseudo-code example given:

sig
type table
val empty : table
val insert : \forall 'a . table -> (string * 'a) -> table
val find : \forall 'a . table -> string -> 'a
end

and I find myself wandering why not parameterize the table type (making it a kind).

Retaining pseudo-code:

sig
kind table['t]
val empty : table[nil]
val insert : \forall 'a . \forall 'b . table['b] -> (string * 'a) -> table['b | 'a]]
val find : \forall 'a . table['a] -> string -> 'a
end

As far as I know this is theoretically sound, or am I mistaken? I am still not comfortable with Haskell syntax so I was unable to decipher the rest of the paper. Any help would be appreciated.

## Comment viewing options

### Need the table to hold multiple types.

• Parameterizing a type makes it a higher-order type, not a kind. An unparameterized type has kind "Type", a type with a single parameter has kind "(Type -> Type)"
• The "*" type operator here creates a tuple type (you may already know this, but I don't understand your return type for "insert".
• Each "\forall" needs to be changed to "\forall 'a".

The goal of the paper was to implement a heterogeneous symbol table, which means the type of the value depends on the associated key.

Here's some Java code that achieves something similar (though it isn't internally type safe):

class TypedKey<T> {}

class Table {
private HashMap<TypedKey<?>,Object> internal
= new HashMap<TypedKey<?>,Object>();

public <T> void put(TypedKey<T> key, T value) {
internal.put(key, value);
}

public <T> T get(TypedKey<T> key) {
return (T) internal.get(key);
}
}

TypedKey<String> NAME = new TypedKey<String>();
TypedKey<Integer> AGE = new TypedKey<Integer>();

Table t = new Table();
t.put(NAME, "Scooby");
t.put(AGE, 42);

System.out.println(t.get(NAME).substring(3));
System.out.println(t.get(AGE) + 5);


### Parameterizing a type makes

Parameterizing a type makes it a higher-order type, not a kind. An unparameterized type has kind "Type", a type with a single parameter has kind "(Type -> Type)"

Yes, my mistake. Thanks for the correction.

The "*" type operator here creates a tuple type (you may already know this, but I don't understand your return type for "insert".

My mistake. I meant to indicate a discriminated union! I've updated the original post.

The goal of the paper was to implement a heterogeneous symbol table, which means the type of the value depends on the associated key.

Ah, now I see!

Thank you very much for your help.