Changes between Version 15 and Version 16 of NewAxioms


Ignore:
Timestamp:
Aug 21, 2012 2:00:34 AM (3 years ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms

    v15 v16  
    33This page describes an extension to type families that supports overlap. 
    44 
    5  * See [https://github.com/dreixel/New-axioms this Github repo] for a Latex draft of the design 
    6  * Here is a [https://docs.google.com/open?id=0B1pOVvPp4fVdOTdjZjU0YWYtYTA5Yy00NmFkLTkxMWUtZmI0NmNhZTQwYzVl cached pdf] of the current state 
    7  * We'll use GHC branch `ghc-axioms` for development work. 
     5 * We'll use GHC branch `overlapping-tyfams` for development work. 
    86 * See also the ''' [wiki:NewAxioms/DiscussionPage Discussion Page] ''' added May 2012, for comment/suggestions/requests for clarification/alternative solutions, to explore the design space. 
    9  * We'll need some concrete syntax for the discussion, so we'll follow the cached pdf, but note that the syntax there is not final. 
     7 * See also the ''' [wiki:NewAxioms/CoincidentOverlap Coincident Overlap] ''' page (added August 2012) for a discussion around the usefulness of allowing certain overlaps when the right-hand sides coincide.  
    108 
    119Status (Jan 12): the groundwork is done, in HEAD; mainly making `CoAxiom` a more fundamental data type.  Not yet started on the details. 
     10 
     11Status (Aug 12): A working prototype implementation is in `overlapping-tyfams`. 
    1212 
    1313== Background ==  
     
    4848== What to do about it == 
    4949 
    50 So the deficiency is in System FC, and it seems fundamental.  We've been working on an extension to System FC, with a corresponding source-language extension, that does allow overlapping type families, with care.  Here's the idea, but do look at the Latex document pointed to from the top of this page for details. 
     50So the deficiency is in System FC, and it seems fundamental.  We've been working on an extension to System FC, with a corresponding source-language extension, that does allow overlapping type families, with care.  Here's the idea of the surface-level extension, but see the attached PDF for the details on the FC extension. (The attached PDF uses the FC formalism fully presented [http://www.cis.upenn.edu/~eir/papers/2013/jmnokinds/jmnokinds.pdf here].) 
     51 
     52All of the following is currently implemented in the `overlapping-tyfams` branch. 
    5153 
    5254 *  A `type instance` declaration can define multiple equations, not just one: 
    5355{{{ 
    54 type instance Equal where 
     56type instance where 
    5557  Equal a a = True 
    5658  Equal a b = False 
     
    6365type family F a :: * 
    6466 
    65 type instance F where 
     67type instance where 
    6668  F [Int] = Int 
    6769  F [a]   = Bool 
    6870 
    69 type instance F where 
     71type instance where 
    7072  F (Int,b) = Char 
    7173  F (a,b)   = [Char] 
    7274}}} 
    7375 
    74  * The groups for `F` may not overlap.  That is, there must be no type `t` such that `(F t)` matches both groups. 
     76 * The groups for `F` may not overlap.  That is, there must be no type `t` such that `(F t)` matches both groups. This rule explicitly excludes overlaps among group members, even if the right-hand sides coincide (but see the [wiki:NewAxioms/CoincidentOverlap Coincident Overlap] page for discussion). 
    7577 
    7678 * The groups do not need to be exhaustive.   If there is no equation that matches, the call is stuck. (This is exactly as at present.) 
    7779 
    78  * It would perhaps be possible to emit warnings for equations that are shadowed: 
     80 * An error is issued when a later equation is matched by a former, making the later one inaccessible. 
    7981{{{ 
    80 type instance F where 
     82type instance where 
    8183  F (a,b)   = [Char] 
    8284  F (Int,b) = Char 
     
    8486  Here the second equation can never match. 
    8587 
     88For closed kinds (and maybe for open ones, but I can't unravel it), it seems possible to write a set of equations that will catch all possible cases but doesn't match the general case. This situation is currently (Aug 2012) undetected, because I (Richard, `eir` at `cis.upenn.edu`) am unconvinced I have a strong enough handle on the details. For example, what about {{{Any}}}? 
     89 
    8690 * The equations do not need to share a common pattern: 
    8791{{{ 
    88 type instance F where 
     92type instance where 
    8993  F Int = Char 
    9094  F (a,b) = Int 
    9195}}} 
    9296 
    93  * Optional extra: It would make sense to allow the `type family` and `type instance` declaration to be combined into one, in cases where all the equations can be given at the definition site.  For example: 
     97 * When matching a use of a type family against a group, special care must be taken not to accidentally introduce incoherence. Consider the following example: 
     98{{{ 
     99type instance where 
     100  F Int = Bool 
     101  F a   = Char 
     102}}} 
     103  and we try to simplify the type {{{F b}}}. The naive implementation would just simplify {{{F b}}} to {{{Char}}}, but this would be wrong. The problem is that {{{b}}} may later be unified with {{{Int}}}, meaning {{{F b}}} should simplify to {{{Bool}}}, not {{{Char}}}. So, the correct behavior is not to simplify {{{F b}}} at all; it is stuck for now. Note that the second equation above is not useless: we will still simplify, say, {{{F Double}}} to {{{Char}}}. 
     104More formally, we only match a type against an equation in an instance group when no previous equation can ''unify'' against the type. 
     105 
     106 * Taking the above point into account, we will still simplify a type family use when those previous unifying equations produce coincident right-hand sides. For example, 
     107{{{ 
     108type instance where 
     109  And True x = x 
     110  And y True = y 
     111}}} 
     112  and we want to simplify {{{And z True}}}. The first equation does not match. The second one does, with the substitution {{{y -> z}}}! But then, the first one unifies with the substitution {{{x -> True, z -> True}}}. Applying both substitutions to the second right-hand side ({{{y}}}) and just the second substitution to the first ({{{x}}}}), we see that both right-hand sides reduce to {{{True}}} in the problematic case (which is when {{{z}}} will unify with {{{True}}} at some later point). So, we can indeed reduce {{{And z True}}} to {{{z}}} as desired. This is indeed a little fiddly, but it seems useful enough to include. 
     113 
     114 * Optional extra (not yet (August 2012) implemented): It would make sense to allow the `type family` and `type instance` declaration to be combined into one, in cases where all the equations can be given at the definition site.  For example: 
    94115{{{ 
    95116type family Equal a b :: Bool where 
     
    103124}}} 
    104125 
    105   
    106126== Questions of syntax == 
    107127 
     
    124144}}} 
    125145We need one of the existing "layout herald" keywords (`of`, `let`, `where`) to smoothly support the nested block of equations.  It's not clear whether or not it is useful to mention the name of the function in the header. 
     146 
     147== Limitations == 
     148 
     149The implementation described above does not address all desired use cases. In particular, it does not work with associated types at all. (Using something like {{{type where}}} in a class definition will be a parse error.) There's no set reason the approach couldn't be expanded to work with associated types, but it is not done yet. In particular, the FC extension will handle intra-module overlapping associated types without a change. 
     150 
     151It seems that inter-module overlapping non-coincident associated types are a Bad Idea, but please add comments if you think otherwise and/or need such a feature. Why is it a Bad Idea? Because it would violate type safety: different modules with different visible instances could simplify type family applications to different ground types, perhaps concluding {{{True ~ False}}}, and the world would immediately cease to exist. 
     152 
     153This last point doesn't apply to overlapping type class instances because type class instance selection compiles to a term-level thing (a dictionary). Using two different dictionaries for the same constraint in different places may be silly, but it won't end the world.