"Nick Kallen" <[EMAIL PROTECTED]> writes:
> > 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'."
How about "makes the implementation much less efficient"? If types
are only present at compile-time, then you don't have to worry about
the running time of functions used in dependent type expressions. If
types are present at run-time, then dependent typing implies that
computations will have parallel computations at the type level,
constantly evaluating what type something is. (Granted, you can
evaluate the types lazily, but this is still a large time cost and a
potential space leak.)
Carl Witty
[EMAIL PROTECTED]
