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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
