Alexander Kuklev (akuklev) wrote,
Alexander Kuklev

Ω : Set -> Set

Various axiomatizations of type theories variously deal with sum types. For one, you can define the type _+_ : (Type, Type) -> Type where
  injr: {A: Type, B: Type} -> A -> (A + B)
  injr: {A: Type, B: Type} -> B -> (A + B)
axiomatically. Or you can define the enumerations and say that sums are dependent pairs:
  A + B = (head: {'left, 'right}) * (value: {'left => A | 'right => B}).

One other elegant option is axiomatic introduction of the Maybe type with constructors
  val a
and its eliminator (default | value => result). It's a very nice solution because you can define lots of useful types a'la carte:

  Nat = Maybe Rec[Nat]
  List (A: Type) = Maybe (A, Rec [List A])
  BTree A = Maybe(A, Rec [BTree A], Rec [BTree A])

  Fin (n: Nat) = (() | prevN => Maybe (Fin prevN))
  Vec (A: Type) (l: Nat) = (() | prevL => (A, (Vec A prevL)))

Note how short and natural primitive recursion looks in this setting:
  add (a: Nat) (b: Nat) = (a || prevB => add (val a) prevB)
  mul (a: Nat) (b: Nat) = (nil || prevB => add a (mul (val a) prevB))

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment


    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.