Re: Avoiding construction of dead dictionaries

We haven't figured out what they did, but the other day we had someone in #haskell with an infinite loop evaluating a dictionary. So apparently it is possible for a dictionary to be bottom somehow. On Mon, Aug 9, 2021 at 11:27 AM Tom Smeding wrote:

Hi Mike,

...

But wouldn't that imply that ghc can build dictionary-construction code

...

that evaluates to bottom? Can that happen?

I assume no, but here the dictionary is embedded as a field in the GADT, right? So if the data value is bottom, there is not even a dictionary to be found, let alone not-bottom.

This assumes that the Dict in `Entail (Sub Dict)` is a GADT like

Dict :: Con b => Dict something

where the Con dictionary is contained in the GADT. Remember that in Core, dictionaries are values, and there is no difference between => and ->.

- Tom

-------- Original Message --------

On 9 Aug 2021, 15:24, Michael Sperber < sperber@deinprogramm.de> wrote:

Thanks for thinking about this one!

On Fri, Aug 06 2021, Tom Smeding wrote:

...

Would it not be unsound for ghc to elide dictionary construction here?

...

After all, the right-hand side might actually be a bottom

...

(e.g. undefined) at run-time, in which case the pattern match cannot

...

succeed according to the semantics of Haskell.

But wouldn't that imply that ghc can build dictionary-construction code

that evaluates to bottom? Can that happen?

...

I suspect that if you make the pattern match lazy (i.e. ~(Entail (Sub

...

Dict))) or ignore the argument altogether (i.e. _), dictionary

...

construction will be elided.

Thanks for the hint! ghc gives me this unfortunately, implying that it

agreed with your first comment:

src/ConCat/Category.hs:190:29: error:

• Could not deduce: Con b arising from a use of ‘r’

from the context: Con a

bound by the type signature for:

(<+) :: forall a b r. Con a => (Con b => r) -> (a |- b) -> r

at src/ConCat/Category.hs:189:1-46

• In the expression: r

In an equation for ‘<+’: r <+ ~(Entail (Sub Dict)) = r

• Relevant bindings include

r :: Con b => r (bound at src/ConCat/Category.hs:190:1)

(<+) :: (Con b => r) -> (a |- b) -> r

(bound at src/ConCat/Category.hs:190:3)

|

190 | r <+ ~(Entail (Sub Dict)) = r

| ^

Other ideas welcome!

--

Regards,

Mike

_______________________________________________

Glasgow-haskell-users mailing list

Glasgow-haskell-users@haskell.org

http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

-- brandon s allbery kf8nh allbery.b@gmail.com