lang/lang/prim.lang

{# 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 = []

  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
}}