Home » forums » LtU Forum

Dynamic Hindley-Milner?

Does anyone know of any work where HM-style type inference is performed at run-time rather than compile time? By this, I mean unification with type variables dynamically using precise (run-time) types.

By Sean McDirmid at 2014-07-07 23:50 | LtU Forum | previous forum topic | next forum topic | other blogs | 4413 reads

Comment viewing options

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

Have you looked at Prolog?

Have you looked at Prolog?

By Matt M at Mon, 2014-07-07 23:58 | login or register to post comments

Sure, and I've implemented

Sure, and I've implemented my fair share of forward and backward chaining systems before. That would be about value unification, what I'm interested in is type unification without backtracking.

By Sean McDirmid at Tue, 2014-07-08 00:05 | login or register to post comments

A Precise Type Is A Value

If its runtime we know that '3' is a type. We can compute algebra by unification of Peano representations of numbers.

So the distinction seems false - a value is a type at runtime. Prolog is almost what you want (without backtracking).

Further backtracking is only relevant if you allow overlapping instances (of functors). If you disallow overlapping, backtracking is not necessary, but it is also not a problem.

One of my side projects is to build an interpreter for dependent types (without lambdas) that is essentially like Prolog without backtracking.

By Keean Schupke at Tue, 2014-07-08 06:25 | login or register to post comments

I guess my type system is

I guess my type system is more hybrid: it has type variables and annotation even if though they are only checked dynamically (for better error reporting). A reified type (whose only use is as a type) would be a value, but not vice versa.

Anyways, it looks like this should just be straightforward unification.

By Sean McDirmid at Tue, 2014-07-08 07:05 | login or register to post comments

I don't get it...

...the point of HM is that you get a most general type, but runtime values are sort of give you most specific types?

Or do you mean you have polymorphic types and type annotations, but you only want to check them dynamically? In that case, you just need to (a) have extra arguments for polymorphic functions, (b) create and pass in a fresh unification variable for each polymorphic type application, and (c) then unify them with type annotations in the conventional way, only at runtime.

If you want to get more mileage out of your annotations, one thing that might be useful to you is Amal Ahmed and Jacob Matthew's Parametric Polymorphism Through Run-Time Sealing, or, Theorems for Low, Low Prices!. This paper extends contract systems to support parametric polymorphism (i.e., it shows how to implement contracts which signal an error if a function uses a polymorphic value non-polymorphically).

By neelk at Tue, 2014-07-08 08:42 | login or register to post comments