#haskell #type-families
Injective type families are a new feature that just got merged with GHC head. Jan Stolarek, Simon Peyton Jones, and I had a paper at Haskell Symposium about them.
The idea is that you can put an injectivity annotation on a type family declaration, which is rather like a functional dependency.
If you want to change selection, open document below and click on "Move attachment"
What are type families? | Types and Kindsw equations can be added to open type families at any time, talking about F2 Char isn’t utterly bogus. But it might be nice to have to assert that an equation for F2 Char is in scope before we use it in a type.
Injective type families
<span>Injective type families are a new feature that just got merged with GHC head. Jan Stolarek, Simon Peyton Jones, and I had a paper at Haskell Symposium about them.
The idea is that you can put an injectivity annotation on a type family declaration, which is rather like a functional dependency. (The injective type family code in this post is not runnable, as it works only with GHC HEAD. The feature will be available with GHC 8.0, due out early 2016.)
type family F3 a = r | r Summary
| status | not read | | reprioritisations | |
|---|
| last reprioritisation on | | | suggested re-reading day | |
|---|
| started reading on | | | finished reading on | |
|---|
Details