[Haskell-cafe] Re: Optimization problem

[apfelmus at quantentunnel.de]

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