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