Improve std and use more implicits

examples/encoding_church.pol

@@ -12,6 +12,6 @@ use "../std/codata/fun.pol"
 
 codata Nat { .iter(A: Type, z: A, s: A -> A): A }
 
-codef S(p: Nat): Nat { .iter(A, z, s) => s.ap(A, A, p.iter(A, z, s)) }
+codef S(p: Nat): Nat { .iter(A, z, s) => s.ap(p.iter(A, z, s)) }
 
 codef Z: Nat { .iter(A, z, s) => z }

examples/encoding_fu_stump.pol

@@ -13,23 +13,23 @@ use "../std/codata/fun.pol"
 
 -- | The type of dependent functions.
 codata Π(A: Type, T: A -> Type) {
-    Π(A, T).dap(A: Type, T: A -> Type, x: A): T.ap(A, Type, x)
+    Π(A, T).dap(A: Type, T: A -> Type, x: A): T.ap(a := A, b := Type, x)
 }
 
 -- | An abbreviation of the induction step, i.e. a function from "P x" to "P (S x)".
 codef StepFun(P: Nat -> Type): Fun(Nat, Type) {
-    .ap(_, _, x) => P.ap(Nat, Type, x) -> P.ap(Nat, Type, S(x))
+    .ap(_, _, x) => P.ap(a := Nat, b:= Type, x) -> P.ap(a := Nat, b:= Type, S(x))
 }
 
 codata Nat {
-    (n: Nat).ind(P: Nat -> Type, base: P.ap(Nat, Type, Z), step: Π(Nat, StepFun(P)))
-        : P.ap(Nat, Type, n)
+    (n: Nat).ind(P: Nat -> Type, base: P.ap(a := Nat, b:= Type, Z), step: Π(Nat, StepFun(P)))
+        : P.ap(a := Nat, b:= Type, n)
 }
 
 codef Z: Nat { .ind(P, base, step) => base }
 
 codef S(m: Nat): Nat {
     .ind(P, base, step) =>
         step.dap(Nat, StepFun(P), m)
-            .ap(P.ap(Nat, Type, m), P.ap(Nat, Type, S(m)), m.ind(P, base, step))
+            .ap(a := P.ap(a := Nat, b:= Type, m), b:= P.ap(a := Nat, b:= Type, S(m)), m.ind(P, base, step))
 }

examples/encoding_parigot.pol

@@ -12,6 +12,6 @@ use "../std/codata/fun.pol"
 
 codata Nat { .analyze(A: Type, z: A, s: Nat -> A -> A): A }
 
-codef S(p: Nat): Nat { .analyze(A, z, s) => s.ap(Nat, A -> A, p).ap(A, A, p.analyze(A, z, s)) }
+codef S(p: Nat): Nat { .analyze(A, z, s) => s.ap(p).ap(p.analyze(A, z, s)) }
 
 codef Z: Nat { .analyze(A, z, s) => z }

examples/encoding_scott.pol

@@ -12,6 +12,6 @@ use "../std/codata/fun.pol"
 
 codata Nat { .case(A: Type, z: A, s: Nat -> A): A }
 
-codef S(p: Nat): Nat { .case(A, z, s) => s.ap(Nat, A, p) }
+codef S(p: Nat): Nat { .case(A, z, s) => s.ap(p) }
 
 codef Z: Nat { .case(A, z, s) => z }

std/codata/fun.pol

@@ -1,7 +1,7 @@
 -- | The type of non-dependent functions.
 codata Fun(a b: Type) {
     -- | Application of a function to its argument.
-    Fun(a, b).ap(a b: Type, x: a): b
+    Fun(a, b).ap(implicit a b: Type, x: a): b
 }
 
 -- | The polymorphic identity function.

std/codata/pair.pol

@@ -1,9 +1,9 @@
 -- | The codata type of pairs defined by a first and second projection.
 codata Pair(a b: Type) {
     -- | First projection on a pair.
-    Pair(a, b).fst(a b: Type): a,
+    Pair(a, b).fst(implicit a b: Type): a,
     -- | Second projection on a pair.
-    Pair(a, b).snd(a b: Type): b
+    Pair(a, b).snd(implicit a b: Type): b
 }
 
 -- | Constructing an element of the pair type.

std/codata/pi.pol

@@ -0,0 +1,6 @@
+use "./fun.pol"
+
+-- | The dependent function type.
+codata Π(a: Type, p: a -> Type) {
+    Π(a, p).dap(a: Type, p: a -> Type, x: a): p.ap(x)
+}

std/codata/sigma.pol

@@ -0,0 +1,7 @@
+use "./fun.pol"
+
+-- | The (strong) Sigma type defined by first and second projections.
+codata Σ(A: Type, T: A -> Type) {
+  Σ(A,T).π₁(A: Type, T: A -> Type): A,
+  (self: Σ(A,T)).π₂(A: Type, T: A -> Type): T.ap(self.π₁(A,T))
+}

std/codata/stream.pol

@@ -1,9 +1,9 @@
 -- | The codata type of infinite streams.
 codata Stream(a: Type) {
     -- | The head observation which yields the first element.
-    Stream(a).hd(a: Type): a,
+    Stream(a).hd(implicit a: Type): a,
     -- | The tail observation which yields the remainder of the stream.
-    Stream(a).tl(a: Type): Stream(a)
+    Stream(a).tl(implicit a: Type): Stream(a)
 }
 
 -- | An infinite stream which repeats the argument.

std/data/bool.pol

@@ -56,7 +56,7 @@ def Bool.nand(other: Bool): Bool {
 
 -- | If-then-else combinator which returns the `then` argument if the boolean is true
 -- | and the `else` argument otherwise.
-def Bool.ite(a: Type, then else: a): a {
+def Bool.ite(implicit a: Type, then else: a): a {
     T => then,
     F => else
 }

std/data/sigma.pol

@@ -0,0 +1,6 @@
+use "../codata/fun.pol"
+
+-- | The Sigma type defined by a toupling constructor.
+data Σ(A: Type, T: A -> Type) {
+  ΣSum(A: Type, T: A -> Type, x: A, w: T.ap(x)): Σ(A,T)
+}