[Haskell-cafe] Re: Optimization problem
apfelmus at quantentunnel.de
apfelmus at quantentunnel.de
Tue Sep 19 14:06:07 EDT 2006
Conor McBride wrote:
> Just imagine
>
>> data Eq a b where Refl :: Eq a a
>
>> coerce :: Eq a b -> a -> b
Robert Dockins wrote:
>>> coerce ~Refl x = x
>
> coerce undefined True :: String
>
> Bang you're dead. Or rather... Twiddle you're dead.
Mom, he's scaring me! ;)
Who says this function may not be strict in the first argument despite
the irrefutable pattern? Also, for the sarcastically inclined, death is
semantically equivalent to _|_. As is (fix id :: a -> b), too.
Alas, one can say
dontcoerce :: Eq a (Maybe b) -> a -> Maybe b
dontcoerce ~Refl x = Just x
and
dontcoerce' _|_ ==> (\x -> Just (x :: b(~Refl)))
==> \(x::_|_) -> Just (x :: _|_)
==> \_ -> Just _|_
The type of x on the right-hand side inherently depends on ~Refl and
should be _|_ if ~Refl is. Type refinement makes the types depend on
values, after all.
For our optimization problem, it's only a matter of constructors on the
right hand side. They should pop out before do not look on any
arguments, so it's safe to cry "so you just know, i'm a Just".
Maybe one can remedy things by introducing a _|_ on type-level with the
only inhabitant _|_ :: _|_. That would treat objections Ross Paterson
referenced:
> See the second restriction. Irrefutable patterns aren't mentioned
> there, but they're the general case. See also
>
> http://www.haskell.org/pipermail/haskell-cafe/2006-May/015609.html
> http://www.haskell.org/pipermail/glasgow-haskell-users/2006-May/010278.html
Admittedly, it's a thin ice to trample on, but otherwise, for this
special splitSeq-problem, one runs into the "more haste less speed"
dilemma (i mean Wadler's paper ). Bertram's lazy algorithm actually is
an online-algorithm and it should remain one when making it type safe.
Regards,
apfelmus
More information about the Haskell-Cafe
mailing list