Eta-expansion and existentials (or: types destroy my laziness)
Max Bolingbroke wrote:
Let's start with a simple example of an existential data type:
data Stream a = forall s. Stream s (s -> Maybe (a, s)) ones :: Stream Int ones = cons 1 ones
Unfortunately, 'ones' is just _|_! The reason is that cons is strict in its second argument. The problem I have is that there is no way to define cons which is simultaneously:
1. Lazy in the tail of the list 2. Type safe 3. Non-recursive
Really? Here are two 'cons' that seem to satisfy all the criteria
{-# LANGUAGE ExistentialQuantification #-}
data Stream a = forall s. Stream s (s -> Maybe (a, s))
nil :: Stream a nil = Stream () (const Nothing)
-- One version -- cons :: a -> Stream a -> Stream a -- cons a str = Stream Nothing (maybe (Just (a, Just str)) run) -- where run (Stream s step) = -- step s >>= (\ (a,s) -> return (a, Just (Stream s step)))
-- the second version cons :: a -> Stream a -> Stream a cons a str = Stream (Just (a,str)) step where step Nothing = Nothing step (Just (a, (Stream s step'))) = Just (a, case step' s of Nothing -> Nothing Just (a',s') -> Just (a',(Stream s' step')))
instance Show a => Show (Stream a) where showsPrec _ (Stream s step) k = '[' : go s where go s = maybe (']' : k) (\(a, s) -> shows a . showString ", " $ go s) (step s)
taken :: Int -> Stream a -> Stream a taken n (Stream s step) = Stream (n, s) (\(n, s) -> if n <= 0 then Nothing else maybe Nothing (\(a, s) -> Just (a, (n - 1, s))) (step s))
ones :: Stream Int ones = cons 1 ones
test2 = taken 5 $ ones -- [1, 1, 1, 1, 1, ]
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 The code implements the whole list library, including zip and zipWith. None of the list operations use value recursion. We still can use value recursion to define infinite streams, which are processed lazily. In fact, the sample stream2 of the example is the infinite stream.
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
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
On 19 October 2010 19:01, Dan Doel
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
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
On 22 October 2010 12:03, Dan Doel
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
participants (3)
-
Dan Doel -
Max Bolingbroke -
oleg＠okmij.org