Changes between Version 5 and Version 6 of NewAxioms/Nonlinearity
 Timestamp:
 May 29, 2013 1:40:26 PM (4 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

NewAxioms/Nonlinearity
v5 v6 36 36 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. 37 37 38 Here are some examples, leaving off the {{{type family}}} headers: 38 For example: 39 {{{ 40 type family Equals a b :: Bool 39 41 40 {{{41 42 type instance Equals x y where 42 43 Equals x x = True 43 44 Equals x y = False 44 45 }}} 46 The 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). 45 47 48 In this case the type space is the whole space, but that need not be the case: 46 49 {{{ 50 type family F a b :: * 51 47 52 type instance F Int x where 48 53 F Int Bool = Double 49 54 F Int Int = Char 50 55 F Int a = Bool 56 57 type instance F Bool y = Int 51 58 }}} 59 Here the first `type instance` covers calls of form `(F Int x)`, while the second covers 60 calls of form `(F Bool y)`. 52 61 53 And thiswill be disallowed: 62 All the equations in the `where` part must be part of (i.e. an instance of) the 63 type space declared in the header. For example, this will be disallowed: 54 64 55 65 {{{ 56 type instance G[x] y where57 G[Int] Int = Bool  OK58 G a b = ()  not OK: outside the type space (G[x] y)66 type instance Bad [x] y where 67 Bad [Int] Int = Bool  OK 68 Bad a b = ()  not OK: outside the type space (Bad [x] y) 59 69 }}} 60 70