#6018: Injective type families
------------------------------+---------------------------------------------
Reporter: lunaris | Owner:
Type: feature request | Status: new
Priority: normal | Component: Compiler
Version: 7.4.1 | Keywords: TypeFamilies, Injective
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Testcase:
Blockedby: | Blocking:
Related: |
------------------------------+---------------------------------------------
Injective type families have been discussed several times on the mailing
list and identified as a potentially useful feature.
I've naively attempted a proof-of-concept in GHC. It's almost certainly
incorrect and probably breaks the type system, but I thought it best to
put it here and see if it can be made workable.
In summary, my changes are:
* Add a new keyword, {{{injective}}}, which is available only when the
{{{TypeFamilies}}} extension is enabled. Injective families may then be
defined thus:
{{{
injective family F a :: *
type instance F Int = Bool
type instance F Bool = Int
injective family G a :: *
type instance G a = a
}}}
Syntax is of course completely changeable; I've simply picked one of the
possible designs. Hopefully this won't be subjected to too much bike-
shedding.
* Add the constructor {{{InjFamilyTyCon}}} to {{{TyConRhs}}} and the
family flavour {{{InjectiveFamily}}} to {{{HsSyn}}}. Again, I've opted to
encode injectivity as a flavour rather than (say) a {{{Bool}}} attached to
type families. This is a completely arbitrary choice and may be utterly
stupid.
* Altered the definition of decomposable {{{TyCon}}}s to include
injective families ({{{isDecomposableTyCon}}}). This effectively
introduces a typing rule that says if we have {{{(F a ~ F b)}}} then we
can deduce {{{(a ~ b)}}} ({{{TcCanonical}}}).
* Modified the unifier so that it will attempt to replace saturated
injective families with their left-hand sides where possible
({{{TcUnify}}}). This means that in a function such as:
{{{
f :: F a -> F a
f = ...
}}}
The type of {{{f False}}} is inferred as {{{F Int}}} (i.e., {{{a}}} is
no longer ambiguous).
Some things work, some things don't. For example, the attached file
typechecks, but if I actually try to evaluate {{{f False}}} I get nothing
(not even a Segmentation fault).
See what you think.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6018>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
