[Haskell] need some help with type inference

Hal Daume III hal at cs.utah.edu
Thu Nov 15 19:18:43 EST 2007


Hi Haskellers --

It's been a while since I've frequented this list, but I'm hoping I can 
stir up some help.  My problem isn't Haskell-specific (so please forgive 
the blanket email), but it *is* related to something written in Haskell, 
so hopefully that's sufficient :).

Basically, the deal is that I have a language for which I need type 
inference.  I currently have something hacked together which works "most 
of the time", but I'd really like to do it right.  The problem is that 
the type system is unlike anything I've encountered before.

There are two "base" types, Real and Integer (which I'll call R and I, 
respectively).  In pseudo-Haskell:

 > data Base = R Double | I Integer

Then, a Type is either a Base type or it's an array with *known* bounds 
of Types.  We can thus get matrices by having arrays of arrays.  For 
instance:

 > type Bound = ...
 > data Type = Base Base | Array Bound Type

This would all be well and good.  The complication is that Bounds can 
either be given by integer bounds (eg., "10") or by variables (eg., 
"N").  So, we might write the type of an array of 10 integers as "I[10]" 
or an array of N reals as "R[N]".

Okay, so that's not so bad yet.  The complication is that the Kth bound 
can refer to any of the previous K-1 bounds.  For instance, the type 
"R[N][D[#1]]" means an array of dimension N, each of whose elements is a 
real array of dimension D[n], where n is the first index.  That is, R[5] 
is an array of length D[5].  Necessarily, D is of type I[N].

And now I need to do type inference/type checking in this system.  I 
have a strong feeling it's undecidable, but I'm fine with that.  I don't 
have a problem require type annotations and, at least for the example 
programs I have written in this language, I've only once ever been 
required to write a type annotation even with my very conservative hacky 
type inference.

So the question is: has anyone encountered a type system like this 
before?  Anyone want to offer suggestions?  I think probably it's most 
appropriate to reply off-list, since I don't want to bog the list down.

Best,

  - Hal

p.s., the language is here: http://www.cs.utah.edu/~hal/HBC

-- 
  Hal Daume III --- me AT hal3 DOT name  |  http://hal3.name
  "Arrest this man, he talks in maths."  |  http://nlpers.blogspot.com


More information about the Haskell mailing list