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

2019-03-25 Thread Anthony Clayden
On Tue, Mar 26, 2019 at 1:05 AM Simon Peyton Jones wrote: Whoa, whoa. Your reply is making a number of presuppositions, and putting words in my mouth I did not say. Firstly: I am totally in favour of a typed intermediate language. Then the question is what type-theory do we use within the IR?

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

2019-03-25 Thread Simon Peyton Jones via Glasgow-haskell-users
I'd far rather see GHC's implementation of FunDeps made more coherent (and learning from Hugs) than squeezing it into the straitjacket of System FC and thereby lose expressivity. To call System FC a straitjacket is to suggest that there is a straightforward alternative that would serve the

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

2019-03-25 Thread Anthony Clayden
> 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