Does this able to proof function extensionality?

[dannypsnl]

For example, in cubical Agda

funExt : ∀ {ℓ} {A : Set ℓ} {B : A → Set ℓ} {f g : (x : A) → B x} →
           ((x : A) → f x ≡ g x) → f ≡ g
funExt p i x = p x i

[xieyuheng]

No, it can not yet prove function extensionality.

Translated to cicada, the function will be:

function funExt(
  A: Type,
  B: (A) -> Type,
  f: (x: A) -> B(x),
  g: (x: A) -> B(x),
  h: (x: A) -> Equal(B(x), f(x), g(x)),
): Equal((x: A) -> B(x), f, g) {
  return TODO
}

[xieyuheng]

@dannypsnl How do you like the JavaScript-like syntax?

I was thinking about sexp-based syntax again.

(designing syntax feels tormenting.)

[xieyuheng]

Something like this:

(define-datatype Nat () ()
  [zero () Nat]
  [add1 ([prev Nat]) Nat])

(claim add (-> Nat Nat Nat))
(define (add x y)
  (induction (x)
    [zero () y]
    [add1 (prev) almost
      ((send Nat add1) (send almost prev))]))

(claim add-commute
  (Pi ([x Nat] [y Nat])
    (Equal Nat (add x y) (add y x))))
(define add-commute
  (induction/motive (x)
    (lambda (x) (Equal Nat (add x y) (add y x)))
    [zero () (add-zero-commute y)]
    [add1 (prev) almost
     (equal-compose
      (equal-map (send almost prev) add1)
      (equal-swap (add-add1-commute y prev)))]))

(define-class Group (Monoid)
  (claim inv (-> Element Element))

  (claim inv-left
    (Pi ([x Element])
      (Equal Element (mul (inv x) x) id)))

  (claim inv-right
    (Pi ([x Element])
      (Equal Element (mul x (inv x)) id)))

  (claim div (-> Element Element Element))
  (define (div x y) (mul x (inv y))))

[dannypsnl]

@dannypsnl How do you like the JavaScript-like syntax?

I was thinking about sexp-based syntax again.

(designing syntax feels tormenting.)

JS-like syntax is fine, in fact, JS-like is easier to find out parameter's type. The only thing I would complain here is cannot write f g : (x : A) -> B(x).

For s-exp, I think cur is a good reference, though it's unification would get limited by its foundation: turnstile.

I'm not sure about class since I'm pretty sure every implementation has some problem when distinguish implementation XD.

[dannypsnl]

return TODO is like postulate in Agda?

[xieyuheng]

TODO is typed hole, not as good as Agda's.

For example (in the REPL):

[xieyuheng]

Once I supported f g : (x : A) -> B(x), but rolled back later, to keep the grammar simple.

Maybe support it again, maybe not.

[xieyuheng]

I see how cur uses : as infix notation, which is not as hardcore as I was thinking about, lol.

[xieyuheng]

Here is a hardcore schemer's sexp:

(claim fun-ext
  (Pi ([A Type]
       [B (-> A Type)]
       [f g (Pi ([x A]) (B x))]
       [h (Pi ([x A]) (Equal (B x) (f x) (g x)))])
    (Equal (Pi ([x A]) (B x)) f g)))

(define fun-ext TODO)

[dannypsnl]

I feel ok with infix notation in s-exp is because now they're scoped XD, the problem is unlimited infix syntax I thought.

[dannypsnl]

close since answered, and maybe I should go to discussion next time lol