Trouble with injective type families

gkaracha george.karachalias at gmail.com
Sat Jul 15 10:48:41 UTC 2017


Me and Tom Schrijvers recently got a paper accepted at Haskell '17 concerning
the elaboration of functional dependencies in System FC *without extending
it*:

     https://people.cs.kuleuven.be/~george.karachalias/papers/fundeps.pdf
<https://people.cs.kuleuven.be/~george.karachalias/papers/fundeps.pdf>  

The work is not currently implemented in GHC but we made some extra effort
to make our system GHC-compatible so that integration will be possible in
the future :-) In addition to the elaboration of FDs, we also noticed that
they are unsound as currently implemented (Section 2.2 in the draft), if we
treat them as type-level functions. Hence, we had to tighten up the
restrictions imposed on them, good thing that until now they didn't affect
the generated System FC code!

There is still some work to be done to transfer the results to injective
type families but I believe we are getting there :)

Cheers,
George



--
View this message in context: http://haskell.1045720.n5.nabble.com/Trouble-with-injective-type-families-tp5860108p5860731.html
Sent from the Haskell - Glasgow-haskell-users mailing list archive at Nabble.com.


More information about the Glasgow-haskell-users mailing list