Changes between Version 5 and Version 6 of NewAxioms/Nonlinearity


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

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/Nonlinearity

    v5 v6  
    3636But, 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. 
    3737 
    38 Here are some examples, leaving off the {{{type family}}} headers: 
     38For example:  
     39{{{ 
     40type family Equals a b :: Bool 
    3941 
    40 {{{ 
    4142type instance Equals x y where 
    4243  Equals x x = True 
    4344  Equals x y = False 
    4445}}} 
     46The header "`type instance Equals x y`" declares the "type space" of the declaration; the `where` part says how to match calls within that type space (top to bottom). 
    4547 
     48In this case the type space is the whole space, but that need not be the case: 
    4649{{{ 
     50type family F a b :: * 
     51 
    4752type instance F Int x where 
    4853  F Int Bool = Double 
    4954  F Int Int  = Char 
    5055  F Int a    = Bool 
     56 
     57type instance F Bool y = Int 
    5158}}} 
     59Here the first `type instance` covers calls of form `(F Int x)`, while the second covers 
     60calls of form `(F Bool y)`. 
    5261 
    53 And thiswill be disallowed: 
     62All the equations in the `where` part must be part of (i.e. an instance of) the  
     63type space declared in the header.  For example, this will be disallowed: 
    5464 
    5565{{{ 
    56 type instance G [x] y where 
    57   G [Int] Int = Bool -- OK 
    58   G a     b   = ()   -- not OK: outside the type space (G [x] y) 
     66type instance Bad [x] y where 
     67  Bad [Int] Int = Bool -- OK 
     68  Bad a     b   = ()   -- not OK: outside the type space (Bad [x] y) 
    5969}}} 
    6070