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

ld be fixed and > *still* translate into FC. If anyone would like to work on that, I’d be > happy to help explain how the current machinery works. > > > > Simon > > > > *From:* Glasgow-haskell-users *On > Behalf Of *Anthony Clayden > *Sent:* 25 March 2019 11:50 &

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

to work on that, I’d be happy to help explain how the current machinery works. Simon From: Glasgow-haskell-users On Behalf Of Anthony Clayden Sent: 25 March 2019 11:50 To: GHC Users List ; Tom Schrijvers Subject: Re: Equality constraints (~): type-theory behind them > On Mon, Dec 10, 2

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

> On Mon, Dec 10, 2018 at 8:36:42 AM Tom Schrijvers wrote: > Maybe our Haskell'17 paper about Elaboration on Functional Dependencies sheds some more light on your problem: Thanks Tom, I've also been working through the 2011 expanded version of 'System F with Type Equality Coercions' that Adam

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

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

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

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.

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: >> >>

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

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

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

Hi Anthony, 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 Cheers, Tom On Sat, Dec 8, 2018 at 6:42 AM Anthony Clayden wrote: > On Fri, 7 Dec 2018 at

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

On Fri, 7 Dec 2018 at 10:57 PM, Adam Gundry wrote: > > Regarding inference, the place that comes to mind is Vytiniotis et al. > OutsideIn(X): > Thanks Adam for the references. Hmm That OutsideIn paper is formidable in so many senses ... I'm not sure I grok your response on my specific q; to

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

Hi AntC [with apologies for the duplicate email], Regarding inference, the place that comes to mind is Vytiniotis et al. OutsideIn(X): Modular type inference with local assumptions. JFP 2011. . On the

Equality constraints (~): type-theory behind them

The (~) constraint syntax is enabled by either `GADTs` or `TypeFamilies` language extension. GADTs/Assoc Data Types/Assoc Type Synonyms/Type Families arrived in a series of papers 2005 to 2008, and IIRC the development wasn't finished in full in GHC until after that. (Superclass constraints took