Changes between Version 7 and Version 8 of TypeNats/Operations


Ignore:
Timestamp:
Jan 27, 2011 5:53:01 AM (4 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Operations

    v7 v8  
    2727== Solving Constraints == 
    2828 
    29 Comparison rules: 
     29There is a set of built-in instances, defining the behavior of each the type-level operations.  These instances are consistent with the theory of arithmetic on natural numbers but they are not complete (i.e., GHC is not perfect at math).  This means that GHC might reject some programs 
     30because it cannot solve all the necessary constraints, even though the constraint can be solved in the general theory of natural numbers.  The most common cause of this is when a programmer writes down a type signature, but GHC infers a slightly different type for the implementation.  Now, GHC needs to check that the specified type is compatible with the implementation.  If it fails do this, then the program will be rejected.  The usual work-around in such situations is to modify the type signature so that it lists explicitly the constraints that GHC could not solve.  If you encounter the same problem often, please consider sending an e-mail to the GHC mailing list to let us know.  We might be able to teach GHC some more math! 
     31 
     32 
     33Basic rules: 
    3034{{{ 
    3135instance m <= n                          -- for concrete numbers m, n with m <= n 
     
    3438instance (a <= b, b <= c) => (a <= c)    -- (under construction) 
    3539 
     40type instance m + n = mn                 -- for concrete numbers m, n, mn, with m + n = mn 
     41type instance 0 + a = a 
     42type instance a + a = 2 * a 
     43type instance a + m = m + a              -- for a concrete number m 
    3644 
     45type instance m + n = mn                 -- for concrete numbers m, n, mn, with m * n = mn 
     46type instance 0 * a = a                    
     47type instance 1 * a = a 
     48type instance a * a = a ^ 2 
     49type instance m * a = a * m              -- for concrete numbers m 
     50 
     51type instance m + n = mn                 -- for conrete numbers m, n, mn, with m ^ n = mn 
     52type instance 1 ^ a = 1 
     53type instance a ^ 0 = 1 
     54type instance a ^ 1 = a 
     55-- type instance a ^ m = a  simplified to a <= 1 
    3756}}} 
     57 
     58 
     59