Changes between Version 15 and Version 16 of NewAxioms/Nonlinearity


Ignore:
Timestamp:
May 29, 2013 2:14:14 PM (2 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/Nonlinearity

    v15 v16  
    2424It's worth noting that {{{-XUndecidableInstances}}} is necessary to exploit this problem. However, we still want {{{-XUndecidableInstances}}} programs to be type-safe (as long as GHC terminates). 
    2525 
    26 == The Solution == 
     26== General idea for the solution == 
    2727 
    2828We need to consider the two instances of {{{F}}} to be overlapping and inadmissible. There are a handful of ways to do this, but the best seems to be this:  
     
    3636 
    3737 
    38  
    39 == Coincident overlap ==  
     38== Problem: coincident overlap ==  
    4039 
    4140In the official release of GHC, it is permitted to write something like this (see [http://www.haskell.org/ghc/docs/latest/html/users_guide/type-families.html#type-family-overlap manual]): 
     
    5352 
    5453 
    55 == Branched instances == 
     54== Problem: branched instances == 
    5655 
    57 But, how does this interact with branched instances (those new instance forms that allow for ordered overlapping)? We still need nonlinear branched instances, as the canonical example of a nonlinear instance is an equality test. The solution is to declare a ''type space'' that all branches fit within. 
     56But, how does this interact with branched instances (those new instance forms that allow for ordered overlapping)? We still need nonlinear branched instances, as the canonical example of a nonlinear instance is an equality test: 
     57{{{ 
     58type family Equals a b :: Bool 
     59 
     60type instance where 
     61  Equals x x = True 
     62  Equals x y = False 
     63}}} 
     64... 
     65 
     66The solution is to declare a ''type space'' that all branches fit within. 
    5867 
    5968For example: