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

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

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)

Heterogenous Collections