Re: Equality constraints (~): type-theory behind them
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 Anthony Clayden < anthony_clay...@clear.net.nz> wrote: > > > 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 Functional Dependencies sheds some more light on your problem: https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/haskell2017a.pdf >>> >> I feel I'm not getting much light shed. No amount of adding `(~)` in GHC >> nor `TypeCast`+`typeCast` method in Hugs will get #9627 function `f` to >> compile. So my 'specific example' earlier in this thread shows `(~)` is >> moderately eager/more eager than FunDeps alone, but not eager enough for >> #9627. >> > > > Can anybody explain @yav's comment here > > https://github.com/ghc-proposals/ghc-proposals/pull/158#issuecomment-449590613 > "currently equality constraints have no run-time evidence associated with > them". > > Haskell has type-erasure semantics. Why would I need any _run-time_ > evidence for anything to do with type improvement? What impact would the > lack of evidence have at run-time? > > Does this mean `(~)` constraints don't produce evidence at compile time? > Which is also the difficulty for type improvement under FunDeps. > > (I tried a type family to achieve the same effect as `(~)` with an > injective TF. No improvement in improvement.) > > > AntC > >> > >> ___ > 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 allber...@gmail.com ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: Equality constraints (~): type-theory behind them
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 Functional Dependencies >>> sheds some more light on your problem: >>> >>> https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/haskell2017a.pdf >>> >>> >> > I feel I'm not getting much light shed. No amount of adding `(~)` in GHC > nor `TypeCast`+`typeCast` method in Hugs will get #9627 function `f` to > compile. So my 'specific example' earlier in this thread shows `(~)` is > moderately eager/more eager than FunDeps alone, but not eager enough for > #9627. > Can anybody explain @yav's comment here https://github.com/ghc-proposals/ghc-proposals/pull/158#issuecomment-449590613 "currently equality constraints have no run-time evidence associated with them". Haskell has type-erasure semantics. Why would I need any _run-time_ evidence for anything to do with type improvement? What impact would the lack of evidence have at run-time? Does this mean `(~)` constraints don't produce evidence at compile time? Which is also the difficulty for type improvement under FunDeps. (I tried a type family to achieve the same effect as `(~)` with an injective TF. No improvement in improvement.) AntC > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: Equality constraints (~): type-theory behind them
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 FunDeps and type improvement ends in 70 ;-) AntC ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: Equality constraints (~): type-theory behind them
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. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: Equality constraints (~): type-theory behind them
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: >> >> https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/haskell2017a.pdf >> >> > Thank you Tom, looks interesting and very applicable. It'll be a few days > before I can take a proper look. > So the paper's main motivation is wrt Trac #9670. I've added some comments there, including a link to your paper. In particular, both GHC and Hugs will infer the 'right' type -- i.e. as improved from the FunDep. But neither allows you to use that improvement to write the desired function `f`. It's a phasing of inference thing(?) I feel I'm not getting much light shed. No amount of adding `(~)` in GHC nor `TypeCast`+`typeCast` method in Hugs will get #9670 function `f` to compile. So my 'specific example' earlier in this thread shows `(~)` is moderately eager/more eager than FunDeps alone, but not eager enough for #9670. IOW from Adam's comment about "inferring where `typeCast` needs to be placed", it seems there's no such place. Perhaps because class `C` has no methods(?) Yes, as per your+Georgios' paper, replacing the FunDep with an Assoc Type and superclass `(~)` constraint is eager enough. That's not telling me why the FunDep+`(~)` constraint on the instances or function signatures isn't so eager. >From the #9670 comment by spj: it's historically to do with an inability to represent evidence under System FC. It seems GHC is taking absence of evidence as evidence of absence, even though it's able to infer the 'right' type. AntC On Fri, 7 Dec 2018 at 10:57 PM, Adam Gundry wrote: >>> ... >>> >>> This is rather like automatically inferring where `typeCast` needs to be placed (indeed, at the Core level there is a construct for casting by an equality proof, which plays much the same role). ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
