dannypsnl / k Goto Github PK
View Code? Open in Web Editor NEWk theorem prover
Home Page: https://pkgs.racket-lang.org/package/k
License: Apache License 2.0
k theorem prover
Home Page: https://pkgs.racket-lang.org/package/k
License: Apache License 2.0
(check (≡ (+ (s z) (s z)) (s (s z)))
(refl))
; error
; cannot-unified: (+ (s z) (s z)) with (s (s z))
The above program cannot work properly, because our naive unification algorithm unifies (+ (s z) (s z))
with (s (s z))
directly. To fix this, we have to check if a term is not normalized, we shall normalize it.
It's easy to find data
's definition is a list of postulate definitions, with such reusing implicit parameters can be done in one place! So I propose the following syntax.
(def f : T
#:postulate)
(def (f [p : P] ...) : T
#:postulate)
And for constructors, syntax will be
(def ...
#:constructor)
Because overlapped binding from racket/base
makes current bounded as constructors is not reliable.
(data Nat : Type
[z : Nat]
[s (n : Nat) : Nat])
to
(def Nat : Type
#:postulate)
(def z : Nat
#:constructor)
(def (s [n : Nat]) : Nat
#:constructor)
(data (≡ {A : Type} [a b : A]) : Type
[refl : (≡ a a)])
to
(def (≡ {A : Type} [a b : A]) : Type
#:postulate)
#|
notice a hard problem here, how to know how many meta came from data type should run into here?
|#
(def (refl {A : Type} {a : A}) : (≡ a a)
#:constructor)
(data (List [A : Type]) : Type
[nil : (List A)]
[:: (a : A) : (List A)])
(data (Vec [E : Type] [LEN : Nat]) : Type
[vnil : (Vec E z)]
[v:: (e : E) (Vec E N) : (Vec E (s N))])
ensure the above program works, and introduce implicit arguments for type automatically(that is, no need to write out {A : Type} -> (List A)
, but just (List A)
).
We have to ensure a definition is covering(no paths get ignored).
Currently, the following code cannot work
(def (identity [a : A]) : A
[a => a])
The current bind is like
(def (foo [x : A] [y : A]) : A
[x => y])
would be good to have
(def (foo [x y : A]) : A
[x => y])
Example from Agda
open import Agda.Builtin.Equality
open import Data.Nat
data Fin : ℕ → Set where
fzero : ∀ {n} → Fin (suc n)
fsuc : ∀ {n} → Fin n → Fin (suc n)
_ : Fin 2
_ = fsuc fzero
_ : Fin 2
_ = fzero
Translated to k
(require k/data/nat)
(data (Fin [n : Nat]) : Type
[fzero : (Fin (s n))]
[fsuc (x : (Fin n)) : (Fin (s n))])
(check (Fin (s (s z)))
fzero)
(check (Fin (s (s z)))
(fsuc fzero))
We can use https://github.com/racket-tw/cover-badge to show test coverage of k.
(data Zero : Type)
(data One : Type
[one : One])
(data Bool : Type
[true : Bool]
[false : Bool])
(data Nat : Type
[z : Nat]
[s (n : Nat) : Nat])
Since now strict positivity check hasn't been enabled, the following program should be type-checked, but not(sadly).
(define-syntax-parser →
[(_ A B) #'(Pi ([x : A]) B)])
(data Bad : Type
[bad [f : (→ ⊥ Bad)] : Bad])
(def (self-app [b : Bad]) : ⊥
[(bad f) (f (bad f))])
(def (absurd) : ⊥
(self-app (bad self-app)))
Error message:
racket.tw/k/k-core/k/core.rkt:77:10: dict-ref: no value found for key
key: #<syntax:3-unsaved-editor:11:12 f>
all keys: '(#<syntax:3-unsaved-editor:10:6 self-app>)
related #3
Or we can define something ridiculous:
(def identity : (-> Nat Nat)
[true => z]
[false => (s z)])
For now, we have to write
(provide Nat s z)
We want
(provide (data-out Nat))
The very basic idea of without-K is that x = x
can't be pattern matched as refl
. The rest of the work of without-K is preventing you from doing the same thing indirectly.
On this, questions are
(define-syntax-parser →
[(_ A B) #'(Pi ([_ : A]) B)])
I guess also rename it out as ->
test.rkt example is not working. Maybe related to #8
; /Users/ar/work/k/example/test.rkt:6:31: x: unbound identifier
; in: x
; Context (plain; to see better errortrace context, re-run with C-u prefix):
; /Users/ar/work/k/core.rkt:58:0 check-type
; .../parse/define.rkt:20:4
; /Users/ar/.emacs.d/elpa/racket-mode-20210727.1545/racket/syntax.rkt:66:0
Do you have more documentation about the package?
For example, the proof
(def (symm [x y : A] [p : (≡ x y)]) : (≡ y x)
[x y refl => refl])
x
, y
, and p
are explicit, but A
is implicit.
The only difference is their syntax-property
so I think they are mergeable.
(check (≡ (* (s z) (s z))
(s (s (s (s (s z))))))
(refl))
(data Bad : Type
[bad [x : (-> Bad X)] : Bad])
avoid bad type, ref to https://github.com/dannypsnl/plt-research/tree/develop/strictly-positive for implementation.
ref to agda: https://agda.readthedocs.io/en/v2.5.2/language/data-types.html#strict-positivity
Need more description for our forms and libraries:
data
def
check
typeof
k/data/nat
k/data/bool
k/data/list
k/data/vec
k/equality
There are many solutions
(def (symm {A : Type}
[x y : A]
[p : (≡ x y)])
: (≡ A y x)
[A x y refl => refl])
When we have different length of definitions (e.g. (≡ x y)
vs (≡ A y x)
), we'll get following errors:
→ racket k-lib/k/equality.rkt
andmap: all lists must have same size
first list length: 4
other list length: 3
procedure: #<procedure:unify?>
context...:
/Applications/Racket v8.3/collects/racket/private/map.rkt:275:2: gen-andmap
/Users/cybai/codespace/racket/k/k-core/k/core.rkt:57:0: check-type
/Applications/Racket v8.3/collects/syntax/parse/private/parse.rkt:1020:13: dots-loop
/Applications/Racket v8.3/collects/syntax/wrap-modbeg.rkt:46:4
however, we should be able to generate the type automatically to do pattern matching.
with a proper implementation, we should be able to see (≡ x y)
and (≡ A x y)
as same thing in the symm
function.
The following program shows problem:
(data (≡ [a : A] [b : A]) : Type
[refl : (≡ a a)])
(check (≡ z z)
(refl))
(check (≡ z (s z))
(refl))
Our unification didn't figure out this program has type mismatching.
#36 constructs an example for it.
(def (fib [n : Nat]) : Nat
[z => z]
[(s z) => (s z)]
[(s (s n)) => (+ (fib (s n))
(fib n))])
The problem came from https://github.com/racket-tw/k/blob/develop/k-core/k/def.rkt#L91-L99; where should bind locals
recursively.
ref: https://github.com/racket-tw/k/blob/develop/k-lib/k/data/nat.rkt#L21-L25
(def (Nat=? [n m : Nat]) : Bool
[z z => true]
[z (s m) => false]
[(s n) z => false]
[(s n) (s m) => (Nat=? n m)])
Error message:
dict-ref: no value found for key
key: #<syntax:k-lib/k/data/nat.rkt:25:19 Nat=?>
all keys: '(#<syntax:k-lib/k/data/nat.rkt:25:6 n> #<syntax:k-lib/k/data/nat.rkt:25:12 m>)
context...:
/Users/dannypsnl/racket.tw/k/k-core/k/core.rkt:73:0: typeof
/Users/dannypsnl/racket.tw/k/k-core/k/core.rkt:56:0: check-type
/Applications/Racket v8.4/collects/syntax/parse/private/parse.rkt:1020:13: dots-loop
/Applications/Racket v8.4/collects/syntax/wrap-modbeg.rkt:46:4
For example:
(def identity : (-> A A)
[m => m])
The interesting part is our CI do not crash
We can have different data type https://arxiv.org/pdf/2103.15408.pdf by @ice1000
A challenge will be how to encode the following behavior.
This pattern matching is not traditional pattern matching, say, it does not need
to be covering (although in the Vec example it is) and it can contain seemingly un-
reachable patterns (like duplicated patterns).
For example, Fin
type:
(data (Fin [n : Nat]) : Type
[(s n) => fzero]
[(s n) => (fsuc [x : (Fin n)])])
There might also have covering type, for example, Vec
type:
(data (Vec [A : Type] [N : Nat]) : Type
[A z => nil]
[A (s n) => (:: [a : A] [v : (Vec A n)])])
The link is how to match brace
And this is required for ≡
type:
(data (≡ {A : Type} [a b : A]) : Type
[refl : (≡ a a)])
(≡ A b c) ; good, apply implicit
(≡ b c) ; good
; same in pattern, full is all implicit
Cubical/HoTT variant language, e.g. #lang k/ube
left
, right
idp
?(def (refl {A : Type}
{a : A})
; `(≡ x y)` is short for `(Path _ x y)`, `Path` is equality in cubical
: (≡ a a)
[{A} {a} => (lambda (i) a)])
; invert is symmetric in cubical
(def (invert [A : Type]
[a b : A]
[p : (≡ a b)])
: (≡ b a)
; The path lambda contains current interval `i`
; to prove reverse result
; we invert the current interval `i` by using `~`
[A a b => (lambda (i) (p (~ i)))])
We should be able to define the following code:
(def (cong {A B : Type}
{x y : A}
[f : (-> A B)]
[P : (≡ x y)])
: (≡ (f x) (f y))
[f refl => refl])
Blocked by #21
The idea is helping constructor expanded as it's name when no parameters, then no transformation would make pattern reference to constructor syntax, then syntax-property
should be accessible.
For example, https://github.com/wilbowma/cur/blob/main/cur/info.rkt. I suppose we will get a layout like
k/info.rkt
k-core/info.rkt
k-lib/info.rkt
k-test/info.rkt
k-doc/info.rkt
k-example/info.rkt
To ensure our type checker works well with ill-form, we need a test set for cases that shall fail.
To now, we still using a simulated pi type(of course make it weaker) that cannot be spread properly. I think now it's a good time to make it correct since it's all things' foundation.
When type checking, unified universe level, and ensure it's a total order. We can build a directed graph that preserves <=
relationship by direction, then a graph without any rings is a valid type-construction.
#lang k
(require k/data/nat
k/data/bool)
(def (Nat-or-Bool [x : Bool]) : Type
[true => Nat]
[false => Bool])
(def a : (Nat-or-Bool true) z)
(def b : (Nat-or-Bool false) true)
The above program shows a simple type depends on the term sample, but it will get:
example/test2.rkt:10:28: type-mismatch: expect: `(Nat-or-Bool true)`, get: `Nat`
The following code shouldn't work but pass our type checking:
(def (foo [x : Nat]) : Bool
[x => x])
This is because we didn't check the function body correctly.
NOTE: Worth taking a look into https://github.com/yjqww6/macrology/blob/master/intdef-ctx.md
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.