Re: [Haskell-cafe] Re: Eta-expansion and existentials (or: types destroy my laziness)
On 19 October 2010 19:01, Dan Doel dan.d...@gmail.com wrote: However, this argument is a bit circular, since that eliminator could be defined to behave similarly to an irrefutable match. Right. Or, put another way, eta expansion of a dictionary-holding existential would result in a value holding a bottom dictionary, whereas that's otherwise impossible, I think. I think evaluating dictionaries strictly is more of a want to have rather than actually implemented. In particular, GHC supports building value-recursive dictionaries - and making dictionary arguments strict indiscriminately would make this feature rather useless. I think this means that even with constrained existential things would be OK. What is definitely not OK is lazy pattern matching on GADTs which have *type equality* constraints on their existentials - because the type equalities are erased at compile time, lazy pattern matching on a GADT would leave no opportunity for us to observe that the proof of the type equality was bogus (a bottom) - so allowing this would let our programs segfault. For example, this program would erroneously typecheck: data Eq a b where Eq :: EQ a a f :: Eq Int Bool - Bool f (~Eq) = ((1 :: Int) + 1) :: Bool main = print $ f undefined I'm sticking with my unsafeCoerce based solution for now. It's ugly, but it's nicely *localised* ugliness :-) Cheers, Max ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Eta-expansion and existentials (or: types destroy my laziness)
On Friday 22 October 2010 5:48:28 am Max Bolingbroke wrote:
I think evaluating dictionaries strictly is more of a want to have
rather than actually implemented. In particular, GHC supports
building value-recursive dictionaries - and making dictionary
arguments strict indiscriminately would make this feature rather
useless.
It now occurs to me that I might be thinking of your paper on strict core.
When does this come up? I only have one example that seems likely:
data Mu f = In { out :: f (Mu f) }
instance Show (f (Mu f)) = Show (Mu f) where
show = show . out
Is that an example of a value recursive dictionary? I also considered:
data AnyShow = forall a. Show a = AS a
instance Show AnyShow where
show (AS x) = AS ( ++ show x ++ )
inf = AS inf
but I don't think the dictionary is actually recursive there. Translating to
explicit dictionary passing seems to confirm the latter impression. The former
is more iffy.
The most obvious way to build a value recursive dictionary would be an
existential like:
inf' = case inf' of AS x - AS (x, x)
but this is prevented from happening by the lack of irrefutable match.
What is definitely not OK is lazy pattern matching on GADTs which have
*type equality* constraints on their existentials.
This is certainly the more compelling deal breaker.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Eta-expansion and existentials (or: types destroy my laziness)
On 22 October 2010 12:03, Dan Doel dan.d...@gmail.com wrote:
data Mu f = In { out :: f (Mu f) }
instance Show (f (Mu f)) = Show (Mu f) where
show = show . out
Is that an example of a value recursive dictionary?
Assuming the Show (f (Mu f)) instance uses the (Mu f) one, AFAIK this
should indeed build a loopy dictionary.
I think this extension was motivated by Scrap your Boilerplate with
Class - see section 5 of
http://research.microsoft.com/en-us/um/people/simonpj/papers/hmap/gmap3.pdf.
Cheers,
Max
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Eta-expansion and existentials (or: types destroy my laziness)
Hi Oleg, Thanks for your reply! Really? Here are two 'cons' that seem to satisfy all the criteria Thanks - your definitions are similar to Roman's suggestion. Unfortunately my criteria 3) is not quite what I actually wanted - I really wanted something GHC-optimisable - (so non-recursive definitions are a necessary but not sufficient condition). The problem is that I'd like to do the static argument transformation on the Stream argument to cons so that GHC can optimise it properly. This is why I've made my cons pattern match on str directly, so the local run/step loop can refer to the lexically bound step/state fields of the stream being consed on to. As Roman suggests, the best way to get GHC to optimise these compositions would be to do something like extend GHC so it can do the SAT by itself :-). Alternatively, a type-safe eta for data types involving existentials would let me do what I want without GHC changes - but I don't think there is a way to define this. Finally, if one doesn't like existentials, one can try universals: http://okmij.org/ftp/Algorithms.html#zip-folds http://okmij.org/ftp/Haskell/zip-folds.lhs I hadn't seen this - thanks! It is certainly a neat trick. I can't quite see how to use it to eliminate the existential I'm actually interested eta-expanding without causing work duplication, but I'll keep thinking about it. Cheers, Max ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Eta-expansion and existentials (or: types destroy my laziness)
On Tuesday 19 October 2010 6:16:16 am Max Bolingbroke wrote: Thanks - your definitions are similar to Roman's suggestion. Unfortunately my criteria 3) is not quite what I actually wanted - I really wanted something GHC-optimisable - (so non-recursive definitions are a necessary but not sufficient condition). ... I hadn't seen this - thanks! It is certainly a neat trick. I can't quite see how to use it to eliminate the existential I'm actually interested eta-expanding without causing work duplication, but I'll keep thinking about it. I doubt it's possible, aside from your unsafeCoerce version. The nub of the problem seems to me to be the lack of irrefutable match on the existential---irrefutable match should be equivalent to eta expanding values, so it's been intentionally disallowed. One could argue that this corresponds to their weak elimination: elim :: (forall a. P a - r) - (exists a. P a) - r However, this argument is a bit circular, since that eliminator could be defined to behave similarly to an irrefutable match. One might expect it to be strict, but it isn't necessary (although it might be difficult to specify how such a lazy reduction would work formally, without resorting to other, stronger elimination principles). Presumably, GHC requires strictness because of constraints that can be bundled in an existential. For one, with local equality constraints, it'd be unsound in the same way that irrefutable matches on a type equality GADT are. However, I also seem to recall that GHC expects all dictionaries to be strictly evaluated (for optimization purposes), while irrefutable matching on a constrained existential would introduce lazy dictionaries. Or, put another way, eta expansion of a dictionary-holding existential would result in a value holding a bottom dictionary, whereas that's otherwise impossible, I think. However, your stream type has no constraints, so there's nothing that would make an irrefutable match unreasonable (unless I'm missing something). I don't expect GHC to start to support this, because, you can only use irrefutable matches on existentials without constraints, is a complicated rule. But I believe that is the core of your troubles, and it doesn't have any necessary connection to type safety in this case. Cheers, -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
