Changes between Version 15 and Version 16 of NewAxioms/Nonlinearity
 Timestamp:
 May 29, 2013 2:14:14 PM (21 months ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

NewAxioms/Nonlinearity
v15 v16 24 24 It's worth noting that {{{XUndecidableInstances}}} is necessary to exploit this problem. However, we still want {{{XUndecidableInstances}}} programs to be typesafe (as long as GHC terminates). 25 25 26 == The Solution ==26 == General idea for the solution == 27 27 28 28 We 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: … … 36 36 37 37 38 39 == Coincident overlap == 38 == Problem: coincident overlap == 40 39 41 40 In the official release of GHC, it is permitted to write something like this (see [http://www.haskell.org/ghc/docs/latest/html/users_guide/typefamilies.html#typefamilyoverlap manual]): … … 53 52 54 53 55 == Branched instances ==54 == Problem: branched instances == 56 55 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. 56 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: 57 {{{ 58 type family Equals a b :: Bool 59 60 type instance where 61 Equals x x = True 62 Equals x y = False 63 }}} 64 ... 65 66 The solution is to declare a ''type space'' that all branches fit within. 58 67 59 68 For example: