Re: Equality constraints (~): type-theory behind them

2018-12-22 Thread Brandon Allbery
I think the point is more that runtime evidence means passing an additional type witness around, potentially changing generated code and even behavior (if this causes dictionary passing where none had been needed previously). It's not addressing your question. On Sat, Dec 22, 2018 at 11:48 PM

Re: Equality constraints (~): type-theory behind them

2018-12-22 Thread Anthony Clayden
On Sat, 22 Dec 2018 at 7:08 PM, Anthony Clayden < anthony_clay...@clear.net.nz> wrote: > > On Mon, 10 Dec 2018 at 6:12 PM, Anthony Clayden < > anthony_clay...@clear.net.nz> wrote: > >> On Mon, 10 Dec 2018 at 9:36 PM, Tom Schrijvers wrote: >> >>> Maybe our Haskell'17 paper about Elaboration on

Re: Equality constraints (~): type-theory behind them

2018-12-22 Thread Anthony Clayden
On Sat, 22 Dec 2018 at 8:01 PM, Oliver Charles wrote: On Sat, Dec 22, 2018 at 11:08 AM Anthony Clayden > wrote: > > > So the paper's main motivation is wrt Trac #9670. > > Are you sure you mean #9670? > Oops. Thanks for the catch Oliver. That should be #9627. (One of the tickets to do with

Re: Equality constraints (~): type-theory behind them

2018-12-22 Thread Oliver Charles
On Sat, Dec 22, 2018 at 11:08 AM Anthony Clayden wrote: > So the paper's main motivation is wrt Trac #9670. Are you sure you mean #9670? https://ghc.haskell.org/trac/ghc/ticket/9670 is "Make Data.List.tails a good producer for list fusion" and has nothing to do with functional dependencies.

Re: Equality constraints (~): type-theory behind them

2018-12-22 Thread Anthony Clayden
On Mon, 10 Dec 2018 at 6:12 PM, Anthony Clayden < anthony_clay...@clear.net.nz> wrote: > On Mon, 10 Dec 2018 at 9:36 PM, Tom Schrijvers wrote: > >> Maybe our Haskell'17 paper about Elaboration on Functional Dependencies >> sheds some more light on your problem: >> >>