Home » forums » LtU Forum

Type-Safe Casts

From Type-Safe Casts by Stephanie Weirich

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.

By cdiggins at 2007-05-07 23:26 | LtU Forum | previous forum topic | next forum topic | other blogs | 5418 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Need the table to hold multiple types.

There are a couple of confusing things about your signature:

  • 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);
By Kannan Goundan at Tue, 2007-05-08 01:26 | login or register to post comments

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.

By cdiggins at Tue, 2007-05-08 07:01 | login or register to post comments