RE: Haskell 2 -- Dependent types?

[Nick Kallen]

> Watch out here; there may be a limit to how much run-time type
> inspection it is reasonable to do in the presence of dependent types.
> Suppose you're examining a type which happens to be the type of some
> sorting function:
>   (Ord a) => (l :: [a]) -> ((l' :: [a]), sorted l l')
> How much type inspection are you willing to allow on that?  How much
> good will it do you?

I'm willing to allow any amount of inspection. Type inspection wrt/ dynamic
types is more useful for doing OO style stuff, and things like apply (cf
previous email on this topic), so I can't imagine a circumstance where one
would actually want to inspect types as detailed as the example you give.
But unless you provide an argument like "this makes programming in the
language more complicated" or "makes implementation impossible", I'm not
willing to draw some arbitrary line: "no inspection beyond `foo'."