GHC: Ticket Query
http://ghc.haskell.org/trac/ghc/query?status=!closed&owner=jstolarek&order=priority
The Glasgow Haskell Compileren-USGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/query?status=!closed&owner=jstolarek&order=priority
Trac 1.0.1
http://ghc.haskell.org/trac/ghc/ticket/6018
http://ghc.haskell.org/trac/ghc/ticket/6018#6018: Injective type familiesWed, 18 Apr 2012 16:22:24 GMTlunaris<p>
Injective type families have been discussed several times on the mailing list and identified as a potentially useful feature.
</p>
<p>
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.
</p>
<p>
In summary, my changes are:
</p>
<ul><li>Add a new keyword, <tt>injective</tt>, which is available only when the <tt>TypeFamilies</tt> extension is enabled. Injective families may then be defined thus:
</li></ul><pre class="wiki"> injective family F a :: *
type instance F Int = Bool
type instance F Bool = Int
injective family G a :: *
type instance G a = a
</pre><blockquote>
<p>
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.
</p>
</blockquote>
<ul><li>Add the constructor <tt>InjFamilyTyCon</tt> to <tt>TyConRhs</tt> and the family flavour <tt>InjectiveFamily</tt> to <tt>HsSyn</tt>. Again, I've opted to encode injectivity as a flavour rather than (say) a <tt>Bool</tt> attached to type families. This is a completely arbitrary choice and may be utterly stupid.
</li></ul><ul><li>Altered the definition of decomposable <tt>TyCon</tt>s to include injective families (<tt>isDecomposableTyCon</tt>). This effectively introduces a typing rule that says if we have <tt>(F a ~ F b)</tt> then we can deduce <tt>(a ~ b)</tt> (<tt>TcCanonical</tt>).
</li></ul><ul><li>Modified the unifier so that it will attempt to replace saturated injective families with their left-hand sides where possible (<tt>TcUnify</tt>). This means that in a function such as:
</li></ul><pre class="wiki"> f :: F a -> F a
f = ...
</pre><blockquote>
<p>
The type of <tt>f False</tt> is inferred as <tt>F Int</tt> (i.e., <tt>a</tt> is no longer ambiguous).
</p>
</blockquote>
<p>
Some things work, some things don't. For example, the attached file typechecks, but if I actually try to evaluate <tt>f False</tt> I get nothing (not even a Segmentation fault).
</p>
<p>
See what you think.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/6018#changelog
http://ghc.haskell.org/trac/ghc/ticket/8317
http://ghc.haskell.org/trac/ghc/ticket/8317#8317: Optimize tagToEnum# at Core levelTue, 17 Sep 2013 12:31:49 GMTjstolarek<p>
Old comparison primops that returned Bool were implemented by inserting call to <tt>tagToEnum#</tt> in the code generator. This call to <tt>tagToEnum#</tt> was later optimized away by a special case in the code geenrator (see <a href="/trac/ghc/browser/ghc/compiler/codeGen/StgCmmExpr.hs">compiler/codeGen/StgCmmExpr.hs</a>, Note [case on bool])). Now that we have new comparison primops (see <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/6135" title="feature request: Unboxed Booleans (closed: fixed)">#6135</a>) we no longer insert <tt>tagToEnum#</tt> in the code generator - all uses of <tt>tagToEnum#</tt> come from explicit calls in a source program. But we still have that special case in the code generator to optimize away <tt>tagToEnum#</tt>. We should drop that special case in the code generator and handle scrutinizing of <tt>tagToEnum#</tt> at the Core level by:
</p>
<ol><li>removing call to <tt>tagToEnum#</tt> in the scrutinee
</li><li>adding calls to <tt>dataToTag#</tt> in case branches
</li><li>constant-folding inserted <tt>dataToTag#</tt>
</li></ol><p>
Here is an example. This Haskell code:
</p>
<pre class="wiki">if tagToEnum# (a ># b)
then E1
else E2
</pre><p>
will be translated to this Core:
</p>
<pre class="wiki">case tagToEnum# (a ># b) of
True -> E1
False -> E2
</pre><p>
and optimized like this:
</p>
<pre class="wiki">case a ># b of
dataToTag# True -> E1
dataToTag# False -> E2
</pre><p>
====>
</p>
<pre class="wiki">case a ># b of
1 -> E1
0 -> E2
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/8317#changelog