[Haskell-cafe] Re: Eta-expansion and existentials (or: types destroy my laziness)

[Dan Doel]

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