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