{# type Type #} ,

{# class Class #} ,

-- Classes

Semigroup : Type -> Class,
Semigroup = a -> {{
  append : a -> a -> a
}},

Monoid : Type -> Class,
Monoid = a -> {{
  semigroup : {{ Semigroup a }},
  empty : a
}},

-- Types

Void : Type,
Void = {
  Void : Type,
  Void = a,

  semigroup : {{ Semigroup Void }},
  semigroup = {{
    append = []
  }},
},

Unit : Type,
Unit = {
  Unit : Type,
  Unit = {},

  semigroup : {{ Semigroup Unit }},
  semigroup = {{
    append = _ _ -> {},
  }},

  monoid : {{ Monoid Unit }},
  monoid = {{
    empty = {},
  }},
},


{# prim bool Bool #},
Bool : Type,
Bool = {
  Bool : Type,
  Bool = [false : {}, true : {}],

  Any : Type,
  Any = {
    semigroup : {{ Semigroup Bool }},
    semigroup = {{
      append = a -> [false = a, true = true],
    }},

    monoid : {{ Monoid Bool }},
    monoid = {{ empty = false }},
  },

  All : Type,
  All = {
    semigroup : {{ Semigroup Bool }},
    semigroup = {{
      append = a -> [false = false, true = a],
    }},

    monoid : {{ Monoid Bool }},
    monoid = {{ empty = true }},
  },
},


Int : Type,
Int = {
  {# prim i64 Int #},
  Int : Type,
  Int = [zero : {}, succ : Nat ],

  Additive : Type,
  Additive = {
    semigroup : {{ Semigroup Int }},
    semigroup = {{
      append = n -> [zero = n, succ = m -> succ (append n m) ],
    }},

    monoid : {{ Monoid Int }},
    monoid = {{
      empty = zero,
    }},
  },

  Multiplicative : Type,
  Multiplicative = {
    semigroup : {{ Semigroup Int }},
    semigroup = {{
      append = n -> [zero = zero, succ = m -> Additive.append n (append n m) ],
    }},

    monoid : {{ Monoid Int }},
    monoid = {{
      empty = succ zero,
    }},
  },
},

Pair : Type,
Pair = {
  Pair : Type -> Type -> Type,
  Pair = a -> b -> { left : a, right : b },

  semigroup : {{ Semigroup A }} -> {{ Semigroup B }} -> {{ Semigroup (Pair A B) }},
  semigroup = {{
    append = { a0, b0 } { a1, b1 } -> { append a0 a1, append b0 b1 }
  }},

  monoid : {{ Monoid A }} -> {{ Monoid B }} -> {{ Monoid (Pair A B) }},
  monoid = {{
    empty = { empty, empty },
  }},
},

Either : Type,
Either = {
  Either : Type -> Type -> Type,
  Either = a b -> [ left : a, right : b ],

  Left : Type,
  Left = {
    semigroup : {{ Semigroup (Either A B) }},
    semigroup = {{
      append = l _ -> l,
    }},
  },

  Right : Type,
  Right = {
    semigroup : {{ Semigroup (Either A B) }},
    semigroup = {{
      append = _ r -> r
    }},
  },
},

List : Type,
List = {
  List : Type -> Type,
  List = a -> [ nil : {} , cons : { head : A , tail : List a } ],

  semigroup : {{ Semigroup (List a) }},
  semigroup = {{
    append = [
      nil  = {}      -> b -> b,
      cons = {a, as} -> b -> cons a (append as b),
    ],
  }},

  monoid : {{ Monoid (List a) }},
  monoid = {{
    empty = nil,
  }},
},

{# prim char Char #},
Char : Type,

{# prim string String #},
String : Type,
String = List Char,

{# builtin show Show #},
Show : Type -> Class,
Show = a -> {{
  show : a -> String,
}},