Unlike incr or inductive, this time I check type statically, so the module system would not exist for type bindings.

The following ridiculous program was valid:

(data (Pair [A : Type] [B : Type])
  [cons : (A B -> (Pair A B))])
(p : (Pair zero Bool))

This is because the current implementation simply believing all claim statement contains a valid type without check. This is not just about we could have an invalid type, this is also about we cannot have dependent function works. For example:

(N-or-B : (Bool -> Type))
(N-or-B =
  (λ (b)
    (match b
      [true => Nat]
      [false => Bool])))
(n : (N-or-B true))
(n = zero)

The above program was valid but also won't work since the current implementation parsed it as N-or-B is a type dependent on a Bool.

non-dependent: A -> B
dependent syntax: (x : A) -> B

Termination checking is required to avoid endless type checking since something like the dependent function existed in a dependent type language.

Primitive Recursion

(+ : (Nat Nat -> Nat))
(+ = (λ (n m)
  (match {n m}
    ; existed the smallest case for n
    [zero ,m => m]
    ; this local n get smaller then origin n(has value (suc n)) obviously
    ; m didn't decrease, but since n eventually terminate this process so that was fine
    [(suc ,n) ,m => (suc (+ n m))])))

(Nat=? : (Nat Nat -> Bool))
(Nat=? = (λ (n m)
  (match {n m}
    [zero zero => true]
    [zero (suc ,m) => false]
    [(suc ,n) zero => false]
    [(suc ,n) (suc ,m) => (Nat=? n m)])))

In this case, a given argument must have exactly one constructor that was smaller in each recursive call.

Structural Recursion

(fib : (Nat -> Nat))
(fib = (λ (n)
  (match {n}
    [zero => zero]
    [(suc zero) => (suc zero)]
    ; k = (suc (suc ,n))
    ; (+ (k-2) (k-1))
    [(suc (suc ,n)) => (+ (fib n) (fib (suc n)))])))

(ack : (Nat Nat -> Nat))
(ack = (λ (n m)
  (match {n m}
    [zero ,m => (suc m)]
    [(suc ,n) zero => (ack n (suc zero))]
    [(suc ,n) (suc ,m) => (ack n (ack (suc n) m))])))

Curry's paradox

F := if C, then F. The claim shouldn't be allowed in a system, else we were able to prove anything since F could be any proposition.

negative example

(data T
      [tt : T -> T -> T])

Reference

• http://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/
• https://link.springer.com/chapter/10.1007/3-540-52335-9_47
• https://lists.chalmers.se/pipermail/agda/2013/006189.html

Here is the classical definition for + of Nat:

(+ : (Nat Nat -> Nat))
(+ = (λ (n m)
  (match {n m}
    [zero ,m => m]
    [(suc ,n) ,m => (suc (+ n m))])))

NOTE: Termination checking would not be considered here and won't be in the near future.

To avoid a constructor accidentally named m and let zero m has a different type than Nat Nat, every variable in the pattern must be pointed out by ,/unquote.

Type checking

;; By λ (n m)
; intros n : ?0, m : ?1, return : ?2
(match {n m}
  ; zero => unify ?0 Nat
  ; ,m : ?3 => unify ?1 ?3
  ; unify ?2 ?3
  [zero ,m => m]
  ; (suc ,n : ?4) => unify Nat ?4
  ; ,m : ?5 => unify ?1 ?5
  ;; application (+ n m)
  ; unify Nat ?4
  ; unify Nat ?5
  ;; application (suc (+ n m))
  ; unify Nat Nat
  ;; result (suc _) : Nat
  ; unify Nat Nat
  [(suc ,n) ,m => (suc (+ n m))])
;; Finally, by (+ : (Nat Nat -> Nat))
unify (Nat Nat -> Nat) (?0 ?1 -> ?2)

Related

This blocks #1

raco setup: error: during making for /typical
137
raco setup: scribblings/typical.scrbl:2:20: module: identifier already required for label
138
raco setup: at: #%top-interaction
139
raco setup: in: typical
140
raco setup: also provided by: typical
141
raco setup: compiling: /typical/scribblings/typical.scrbl
142
raco setup: error: during building docs for /typical/scribblings/typical.scrbl
143
raco setup: scribblings/typical.scrbl:2:20: module: identifier already required for label
144
raco setup: at: #%top-interaction
145
raco setup: in: typical
146
raco setup: also provided by: typical
147
raco setup: location...:
148
raco setup: scribblings/typical.scrbl:2:20
149
raco setup: context...:
150
raco setup: do-raise-syntax-error
151
raco setup: check-not-defined
152
raco setup: for-loop
153
raco setup: [repeats 1 more time]

(data (= [A : Type] [a : A] [b : A])
          [refl : ((a : A) -> (= A a a))])

This type would need some extensions to the language.

A data type

(data C
  [c0 : C]
  [c1 : (C -> C)])

can be

(define c0 'c0)
(define (c1 x) ('c1 x))

we believe type checking is correct anyway.

A claim/define pair

(a : Nat)
(a = z)

can be(remove claim since type-checked)

(define a z)

A lambda

(id : (A -> A))
(id = (λ (x) x))

can be a lambda

(define id (λ (x) x))

Application

(suc zero)

is an application

(suc zero)

A pattern matching

(+ : (Nat Nat -> Nat))
(+ = (λ (n m)
  (match {n m}
    [zero ,m => m]
    [(suc ,n) ,m => (suc (+ n m))])))

is a little bit harder

(match* {n m}
  [{`zero `,m} m]
  [{`(suc ,n) `,m} (suc (+ n m))])

Get error like:

?: invalid statement in: (a = zero)

for valid program

(a : Nat)
(a = zero)