> > > If this is true, then what I'm doing is horrible. But I don't
> see how this
> > > leads to nondeterminism or broken referential transparency.
> min2 returns the
> > > same value for the same list, but it's simply more efficient
> if we happen to
> > > know some more information about the list.
> >
> > In this particular case that happens to be so. But it's not true in
> > general. What if the body of min2 were defined so that it returned
> > something different in the two cases? Your code has no proof that the
> > code for the two cases is equivalent. If it's not, then the behaviour
> > would depend on whether the compiler could deduce that a particular
> > argument had type Sorted or not. And that in turn could depend on the
> > amount of inlining etc. that the compiler does.
I'm not asking the compiler to deduce anything. I'm talking about run-time
type matching; this is dynamic types!
> I would assume that any language with this feature would have a
> precise specification of type inference sufficient to determine which
> of the two cases was used. Without such a specification, portable
> programming with dependent types is impossible; programs would compile
> under one "smart" compiler (which does more inference) and fail with a
> type error on another.
The issue is not determining which of two cases was used. Run time
inspection is sufficient, the issue is whether I'm violating referential
transparency. I've thought about this issue more and have a contrary point.
I'm not violating referential transparency.
Why, because it is *not* unreasonable to assume that two functions will
behave differently for different types.
- ad hoc polymorphism (classes) violate referential transparency by that
argument, doesn't it?
- for subtypes (which is what my example was), it is not unreasonable to
assume that a function will have different behavior for the subtype than for
the supertype. This is obvious in OO programming--overriden methods. This is
further obvious in a dynamic type system where you have functions like:
draw :: Dynamic -> Picture
draw (c :: Circle) = ...
draw (s :: Square) = ...
...
further:
min2 :: Dynamic -> Picture
min2 (l :: SortedList) = hd l
min2 (l :: [a]) = min l
note that here SortedList is just some ADT, not something dependant.
To beat this to death:
min2 :: [a] -> a
min2 (3:ls) = 0
min2 l = min l
In sum, I argue:
Complete runtime type inspection on dependant (sub)types violates nothing
that anything else we already have doesn't.
