traits.myr

   1 use std
   2
   3 pkg yakmo =
   4         /* "ip" stands for "in place". The first argument is modified. */
   5
   6         /* 0, +, - */
   7         trait group_struct @a =
   8                 gid  : (-> @a)
   9                 eq_gid : (a : @a -> bool)
  10                 gadd_ip : (a : @a, b : @a -> void)
  11                 gadd : (a : @a, b : @a -> @a)
  12                 gneg_ip : (a : @a -> void)
  13                 gneg : (a : @a -> @a)
  14         ;;
  15
  16         /* group, plus · and 1 */
  17         trait ring_struct @r /* :: yakmo.group_struct @r */  =
  18                 rid : (-> @r)
  19                 rmul_ip : (a : @r, b : @r -> void)
  20                 rmul : (a : @r, b : @r -> @r)
  21         ;;
  22
  23         /* ·^{-1} */
  24         trait field_struct @k /* :: yakmo.ring_struct @k */ =
  25                 finv : (k : @k -> std.option(@k))
  26         ;;
  27
  28         /*
  29            Ex: Laurent polynomials. [ (x^2 + 1) / y ] / [ (x - 1) / z ]
  30            should be computable as [ (xz + z) / y ], but [ z / (x - 1) ]
  31            is not a finite Laurent polynomial, so [ (x - 1) / z ] need
  32            not have a representable inverse.
  33          */
  34         trait division_struct @d /* :: yakmo.ring_struct @d */ =
  35                 div_maybe : (a : @d, b : @d -> std.option(@d))
  36         ;;
  37
  38         /* phi : ring x module -> module */
  39         trait module_struct @m -> @r :: yakmo.ring_struct @r /*, yakmo.group_struct @m*/ =
  40                 phi_ip : (r : @r, m : @m -> void)
  41                 phi : (r : @r, m : @m -> @m)
  42         ;;
  43
  44         /* these are algebras over rings, so automatically modules */
  45         trait algebra_struct @a -> @r :: yakmo.ring_struct @r, yakmo.module_struct @a -> @r =
  46                 amul_ip : (a : @a, b : @a -> void)
  47                 amul : (a : @a, b : @a -> @a)
  48         ;;
  49
  50         /* absolute value, because I want it without implementing sqrt(x * \bar{x}) */
  51         trait abs_struct @a =
  52                 abs_ip : (a : @a -> void)
  53                 abs : (a : @a -> @a)
  54                 cmp_zero : (a : @a -> std.order)
  55         ;;
  56
  57         /* degree is hardcoded to Z; see polyring.myr for that */
  58
  59         /*
  60            GCD/LCM.
  61
  62            TODO: lists, and all that.
  63
  64            TODO: perhaps merge them.
  65          */
  66         trait gcd_struct @a =
  67                 gcd : (a : @a, b : @a -> @a)
  68         ;;
  69         trait lcm_struct @a =
  70                 lcm : (a : @a, b : @a -> @a)
  71         ;;
  72
  73         /* real structure is just complex conjugation */
  74         trait real_struct @r =
  75                 /* "complex conjugation" */
  76                 compconj_ip : (r : @r -> void)
  77                 compconj : (r : @r -> @r)
  78         ;;
  79
  80         /*
  81            To find the Zlike, &c traits, see Z.myr, Q.myr, &c.
  82          */
  83 ;;