Lambda the Ultimate

Please join us for the next FringeDC informal meeting near the Eastern
Market in Washington DC for beer & talk about stuff (monadic
transformers, Amazon S3, delimited continuations- the typical kind of
stuff people chat about on a Saturday night)

FringeDC is a group for people interested in functional and lisp-like
languages. (Haskell, Erlang, Scheme, CL, etc) Anyone is welcome!

Main Site: www.lisperati.com/fringedc.html
Meeting Info: www.lisperati.com/may12th.html

Formalizing and extending C# type inference (pdf), Gavin Bierman

"Unfortunately this part of the published language specification is a little terse, and hence this feature can often behave in surprising ways for the programmer. Moreover, this process is quite different from the better known one implemented in Java 5.0. In this paper we attempt a formal reconstruction of the type inference process as it is currently implemented in C# 2.0."

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.