I have a situation in which I have two kinds of trees. The simplified example is linked lists:
type foo = [`Nil | `Tree of foo]
type bar = [`Nil | `Leaf of int | `Tree of bar]
I have a tree with only shape, and a tree with some information. I want
to be able to distinguish between these. Here I have functions to
assert types, but these annotations will be part of the signatures of
functions actually doing things in the real code. But I do want to have
these static checks on contests.
let f x : foo = x
let g x : bar = x
let a = `Tree (`Nil)
let b = `Tree (a)
let c = `Tree (f a)
let d = `Tree (`Leaf 1)
As is proper, I can run f on a, b, and c, but not on d. D is not a valid foo.
But I cannot run g on c. This makes sense, as I have said 'a tree of
bars contains a bars.' But I want to somehow note that a tree of bars
MIGHT contain foo's. Is there any way to annotate this?
I cannot say
type bar = [`Nil | `Leaf of int | `Tree of [bar | foo]] as bar is not fully defined.
I cannot say
type bar = [`Leaf of int | `Tree of bar | foo] because tree cannot have two separate types.
The current, icky, non-variant type solution has the equivalent of
type 'a foo = Nil | Tree of foo | F of 'a
With special things filling in for 'a. But I end up putting EVERYTHING
in 'a because I don't have a way to statically guaranteeing that my
"leaf foo"'s are valid "leaf or branch foo's". So I have a weaker
system than I want.
Any suggestions? Seems like variant types should work here. I COULD add
type annotations to functions, check them, and then remove the
annotations so that my types are never constrained. I think that might
even work. But it seems rather icky.
--
Seth Fogarty sfogarty@[gmail.com|rice.edu|livejournal]
Neep-neep at large AIM: Sorrath
"I know there are people in this world who do not love their fellow
human beings - and I hate people like that" --Tom Lehrer.