Type system that can type list structure?

I'm looking for example type systems that can type list structure.

For a simple example... (Sorry, I think in code)

// Map two elts at a time, not two lists
def map2(alist:List, f(*,* -> 'u) -> 'u List) // f(*,*) is not good
def mklis(nl: 'u List, rest: List)
match rest
| a :: b :: r  -> mklis(f(a,b) :: nl, r)  // types of a and b?
| else -> reverse(nl)
in mklis(nil, alist);

def plist2alist(plist:List -> <List>List)
map2(plist, fn(a,b) a :: b :: nil);

plist2alist('(A, 1, B, 2, C, 3))
=> ((A,1),(B,2),(C,3))

It would be very nice to type plist's internal structure,
thus allowing for typing the map2 function, plist2alist()'s
resulting internal structure, etc.

I can sort of imagine some kind of regex typing construct,
but I have no clear ideas on this.  Any languages out there
do a good job of typing repeating internal patterned structure
like this?

If this is impossible for any theoretical reason, I'd love
to know that too :-)

Many thanks.

Scott


Comment viewing options

Look at typing XML

Various systems have been proposed to type XML data, which is a very similar problem. The first example that comes to mind is XDuce, although I'm sure there are many others. XDuce at least does indeed use a notion of "regular expression types" as you suggest. I would look in this area if I were you.

Cat

you might want to bug cdiggins one of the posters around here and author of the Cat programming language, his whole deal is having a typed stack, which seems like a very similar problem.

dependent types?

Try looking at dependent types as in Epigram and others?

I mucked around a bit. Sorry

I mucked around a bit. Sorry if the syntax seems funky, but the idea should come across. Also, if one can slip a constructor into argument list of ConsA, then ConsB could be moved into the definition of List2. This sort of achieves what we might want for a Lisp style property list, but it's not really a list anymore, using a new set of constructors.

class 'h 't ConsB(hd: 'h, tl: 't) ;

class 'a 'b List2 =
ConsA(hd: 'a, tl:ConsB('b, 'a 'b List2))
| Nil2
;


As it stands, it seems to me just an odd way to write ConsA('a, 'b, 'a 'b List2) A pattern match in the first case would look something like.

   | ConsA(k,ConsB(v,r)) -> // Fool with k,v,r values

or this in the second case of a two headed Cons.

| ConsA(k,v,r) -> // Fool with k,v,r values


This gives us something like a well typed property list, but again, it's not really a list - we're not here imposing type structure on a series (repeating or not repeating) of Cons cells. I mean, they are Cons cells, in the ConsA/ConsB case, in the sense that they have head/tail - but they are different types (different constructors).

I can sort of imagine something like the above definition, but somehow just specifying additional constraints on the good old "regular" List and cons cells. Perhaps with would be a kind of subtyping or "inheritance", as in oop? Dunno.

The regular expression idea from XML is also intriguing. Seems like sort of the same problem - imposing typed structure on aggregates that use the same underlying compositional machinery.

Nested data types

You might want to take a look at nested data types.

data Twist a b = Nil | Cons a (Twist b a) deriving Show

map2 _ Nil = Nil
map2 f (Cons x (Cons y rest)) = Cons (f x y) (map2 f rest)

main = do let pl = (Cons "a" (Cons 1 (Cons "b" (Cons 2 (Cons "c" (Cons 3 Nil))))))
print (map2 (,) pl)
print (map2 (flip replicate) pl)