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: