~ Youkai (∞, 1)-Mountain
Home Page: https://www.aya-prover.org
License: MIT License
This is the archieve of the early development of the Aya prover. The development has been moved to https://github.com/aya-prover/aya-dev
![bors[bot] avatar](https://avatars.githubusercontent.com/in/1847?v=4 "bors[bot]")
Neutralization by Elimination
Does that sound like a plan? @re-xyr
I've been thinking about the details of this. Firstly, if we don't have let-expressions, we only have to detect all definitions at the top-level and submodules and form a dependency graph out of it. However if we have let-expressions, I think the solution is like this:
let-expressions);C in some A uses B then A depends on B too);let-expression, we form a dependency graph of the module of the let-expression, typecheck them, and go on.Why not directly form a dependency graph out of all definitions, including those in the let-expressions?
let-expressions, the localCtx has the variables of the outer definition.let-expressions outside like we did to modules; because this way we could not ensure the localCtx. We should typecheck them only when we meet them, at that time the localCtx will be complete.Why won't this cause a problem in dependency?
let-expression depends on another definition outside, then that definition is also depended on by the outer definition of the let-expression. So when we check the let-expression, its dependencies are all checked too.let-expression at all.The following file, when including the last line, cannot type check.
I suspect the normalized form is wrong.
prim I
prim left
prim right
struct Path (A : I -> Type) (a : A left) (b : A right) : Type
| at (i : I) : A i {
| left => a
| right => b
}
def path {A : I -> Type} (p : Pi (i : I) -> A i)
=> new Path A (p left) (p right) { | at i => p i }
def `=` Eq {A : Type} (a b : A) : Type => Path (\ i => A) a b
def idp {A : Type} (a : A) : a = a => path (\ i => a)
bind = looser application
prim arcoe
def hfill2d {A : Type}
{a b c d : A}
(p : a = b)
(q : b = d)
(r : a = c)
(i j : I) : A
=> (arcoe (\ k => (r.at k) = (q.at k)) p i).at j
def hcomp2d {A : Type}
{a b c d : A}
(p : a = b)
(q : b = d)
(r : a = c) : c = d
=> path (hfill2d p q r right)
def sym {A : Type} {a b : A} (p : a = b) : b = a => hcomp2d (idp a) (idp a) p
def `~` trans {A : Type} {a b c : A} (p : a = b) (q : b = c) : a = c => hcomp2d p q (idp a)
def pmap {A B : Type} (f : A -> B) {a b : A} (p : a = b)
: f a = f b => path (\ i => f (p.at i))
-- def funext {A B : Type} (f g : A -> B) (p : Pi (a : A) -> f a = g a) : f = g
-- => path (\ i => \ x => (p x).at i)
def sq {A B C : Type} {a c : A} {b d : B} (f : A -> B -> C) (p : a = c) (q : b = d) : f a b = f c d
=> trans (pmap (f a) q) (pmap (\ x => f x d) p)
def isProp (A : Type) : Type => Pi (x : A) (y : A) -> x = y
def isSet (A : Type) : Type => Pi (x : A) (y : A) -> isProp (x = y)
data Bot : Type
open data Top : Type
| T
open data Nat : Type
| zero
| suc Nat
def `+` add (m n : Nat) : Nat
| zero, n => n
| n, zero => n
| suc m, n => suc (add m n)
| m, suc n => suc (add m n)
def `*` mul (m n : Nat) : Nat
| zero, n => zero
| m, zero => zero
| suc m, suc n => suc (m + n + m * n)
def `*'` mul' (m n : Nat) : Nat
| zero, n => zero
| m, zero => zero
| suc m, n => n + m *' n
def `*''` mul'' (m n : Nat) : Nat
| zero, n => zero
| m, zero => zero
| m, suc n => m + m *'' n
bind + tighter =
bind * tighter +
bind *' tighter +
bind *'' tighter +
def BiOp (A : Type) => A -> A -> A
def Associative {A : Type} (· : BiOp A) => Pi (x y z : A) -> (· x (· y z)) = (· (· x y) z)
def Commutative {A : Type} (· : BiOp A) => Pi (x y : A) -> (· x y) = (· y x)
def Identity {A : Type} (e : A) (· : BiOp A) => Pi (x : A) -> Sig ((· e x) = x) ** ((· x e) = x)
def +-comm (x y : Nat) : x + y = y + x
| zero, n => idp n
| suc n, m => pmap suc (+-comm n m)
def +-assoc (x y z : Nat) : x + (y + z) = (x + y) + z
| zero, y, z => idp _
| suc x, y, z => pmap suc (+-assoc x y z)
def +-identity (x : Nat) : Sig (x + zero = x) ** (zero + x = x)
| x => (idp x, idp x)
def *'-suc (m n : Nat) : m *' (suc n) = m + m *' n
| zero, n => idp _
| suc m, n => (pmap (\ x => suc (add n x)) (*'-suc m n))
~ (pmap suc (+-assoc n m (m *' n)))
~ (pmap (\ x => suc (x + m *' n)) (+-comm n m))
~ (pmap suc (sym (+-assoc m n (m *' n))))
def *'-suc-suc (m n : Nat) : (suc m) *' (suc n) = suc (m + n + m *' n)
=> (pmap (add (suc n)) (*'-suc m n))
~ (pmap suc (+-assoc n m (m *' n)))
~ (pmap (\ x => suc (x + m *' n)) (+-comm n m))
def *'-*''-iso (m n : Nat) : m *' n = m *'' n
| m, zero => idp _
| m, suc n => (*'-suc m n) ~ (pmap (add m) (*'-*''-iso m n))
def *-*'-iso (m n : Nat) : m *' n = m * n
| zero, n => idp _
| m, zero => idp _
| suc m, suc n => (*'-suc-suc m n) ~ (pmap (\ x => suc ((m + n) + x)) (*-*'-iso m n))
def sym-*'-suc-suc (m n : Nat) : suc (m + n + m *' n) = (suc m) *' (suc n) => sym (*'-suc-suc m n)
120 | | suc m, suc n => (*'-suc-suc m n) ~ (pmap (\ x => suc ((m + n) + x)) (*-*'-iso m n))
121 |
122 | def sym-*'-suc-suc (m n : Nat) : suc (m + n + m *' n) = (suc m) *' (suc n) => sym (*'-suc-suc m n)
^-----------------^
Error: Cannot check the expression of type
Path (λ _9 ⇒ Nat) (hfill2d {Nat} {suc (add n (mul' m (suc n)))} {suc (add
n (mul' m (suc n)))} {suc (add (add m n) (mul' m n))} {suc (add n (mul' m (suc
n)))} (idp {Nat} suc (add n (mul' m (suc n)))) (idp {Nat} suc (add n (mul'
m (suc n)))) (*'-suc-suc m n) right left) (hfill2d {Nat} {suc (add n (mul'
m (suc n)))} {suc (add n (mul' m (suc n)))} {suc (add (add m n) (mul' m n))}
{suc (add n (mul' m (suc n)))} (idp {Nat} suc (add n (mul' m (suc n)))) (idp
{Nat} suc (add n (mul' m (suc n)))) (*'-suc-suc m n) right right)
(Normalized: Path (λ _9 ⇒ Nat) (suc (add n (add m (mul' m n)))) (suc (add
n (mul' m (suc n)))))
against the type
Eq {Nat} (suc (add (add m n) (mul' m n))) (mul' (suc m) (suc n))
(Normalized: Path (λ i ⇒ Nat) (suc (add (add m n) (mul' m n))) (suc (add n
(mul' m (suc n)))))
Commit: 1707136
Given the following code:
prim I
prim left
prim right
prim arcoe
struct Path (A : I -> Type) (a : A left) (b : A right) : ooType
| at (i : I) : A i {
| left => a
| right => b
}
def path {A : I -> Type} (p : Pi (i : I) -> A i)
=> new Path A (p left) (p right) { | at i => p i }
def `=` Eq {A : Type} (a b : A) : ooType => Path (\ i => A) a b
def idp {A : Type} (a : A) : a = a => path (\ i => a)
def coe {a b : Type} (eq : a = b) (x : a) (i : I) : eq.at i
=> arcoe eq.at x i
bind = looser application
open data Unit : Set 0 | unit
open data Entity : Set 0
| john
struct EventT : Set 1
| agentT : Set 0
def getAgentT (t : EventT) : Set 0 => t.agentT
def setAgentT (x : Set 0) (t : EventT) : EventT
=> new EventT { | agentT => x }
def agentT-inv {t : EventT} {u : Set 0} : (setAgentT u t).agentT = u
=> idp u
struct Event (t : EventT) : Set 2
| agent : t.agentT
def getAgent (t : EventT) (e : Event t) : t.agentT => e.agent
open data RunImpl (ag : Entity) : Set 0
| john => run1
def Run (e : Event (new EventT { | agentT => Entity })) : Set 3
=> RunImpl e.agent
def mkVerb {t : EventT} (p : Event t -> Set 3) : (Event t -> Set 3) -> Set 3
=> \f => Sig (e : Event t) ** (Sig (p e) ** (f e))
def run : (Event (new EventT { | agentT => Entity }) -> Set 3) -> Set 3
=> mkVerb {new EventT { | agentT => Entity }} Run
def mkTheta
(getT : EventT -> Set 0)
(get : Pi (t : EventT) -> Event t -> getT t)
(setT : Set 0 -> EventT -> EventT)
(invariant : Pi {t : EventT} {u : Set 0} -> u = getT (setT u t))
: Pi {u : Set 0} {t : EventT}
-> ((u -> ooType 3) -> ooType 3)
-> ((Event (setT u t) -> ooType 3) -> ooType 3)
-> (Event (setT u t) -> ooType 3) -> ooType 3
=> \{u} {t} => \q p => \f =>
q (\x => p (\e => Sig (get (setT u t) e = coe invariant x right) ** (f e)))
def agent' :
Pi {u : Set 0} {t : EventT}
-> ((u -> ooType 3) -> ooType 3)
-> ((Event (setAgentT u t) -> ooType 3) -> ooType 3)
-> (Event (setAgentT u t) -> ooType 3) -> ooType 3
=> \{u} {t} => mkTheta getAgentT getAgent setAgentT (\{t'} {u'} => agentT-inv {t'} {u'}) {u} {t}
def mkConst {t : Set} (x : t) : (t -> ooType 3) -> ooType 3
=> \f => f x
def john' : (Entity -> ooType 3) -> ooType 3
=> mkConst john
def mkSentence {t : EventT} (p : (Event t -> ooType 3) -> ooType 3) : ooType 3
=> p (\x => Unit)
def john-runs : ooType 3 =>
mkSentence {new EventT { | agentT => Entity }}
(agent' {Entity} {new EventT { | agentT => Unit }} john' run)
def proof-john-runs-event : Event (new EventT { | agentT => Entity })
=> new Event (new EventT { | agentT => Entity }) { | agent => john }
This code doesn't type check because the function body can't be typed:
def proof-john-runs : john-runs => (proof-john-runs-event, (run1, (idp john, unit)))
The type expected by the compiler was:
Σ (e : Event new { | agentT ⇒ Entity }) ** (_ : Σ (_1 : RunImpl
e.agent) ** (_ : Σ (_7 : Path (λ i ⇒ Entity) e.agent john) ** (_ : Unit)))
So I wrote this, which type checks:
def proof-john-runs-impl
: Sig (e : Event (new EventT { | agentT ⇒ Entity }))
** Sig (RunImpl e.agent)
** (Sig (Path (\i => Entity) e.agent john) ** Unit)
=> (proof-john-runs-event, (run1, (idp john, unit)))
However, this still doesn't type check:
def proof-john-runs : john-runs => proof-john-runs-impl
(Sorry, I couldn't simplify this example; it's too difficult for me.)
As title. I think this is an interesting idea, and I will discuss this with y'all in the next Walpurgis night.
Commit: c7d7714
open data Unit : Type | unit
def foo : Sig Unit ** Unit => (unit, unit)
def bar : Sig Unit ** Unit => foo
Commit: 77e6676
This causes an "unsolved meta" error:
struct Unit : Type
open data Foo (x : Unit) : Type | foo
def foo' : Foo (new Unit {}) => foo
This works, however:
open data Unit : Type | unit
open data Foo (x : Unit) : Type | foo
def foo' : Foo unit => foo
So we should improve it
As title. I'm quite unsure how to do this..
As title
Opened during Walpurgis night
Let me start: a syntax design for a suitable markup language. Obviously we need our own markup language 🤔 and we need to compile it in our Doc backends.
Since we have the blue Aya (i.e. Iizunamaru Megumu) now, who is the leader of Tengu's (incl. Aya), we can consider naming one of our tools Megumu too (such as the package manager, or the installation manager). We may also use mgm as a mysterious abbreviation.
Similar to Agda's forall. Also, we may add exists for Sig.
This means allowing fields/ctors defined later refer to those defined earlier in their types, as what we did to Stmts, as long as the dependency graph forms a DAG.
For structs,
struct A : \Type
| v : T
| T : \Type
For datas,
data B (n : N) : \Type \with
| zero => { | conA (P conC) | conB }
| suc m => { | conC | conD (P conA) }
The case for datas looks more complicated because constructors are intertwined with match clauses.
E.g. "type in type"
As title. Agda has some technical slides, I think we could learn from that.
Currently, we have lots of code duplicated in the 'success' test folder. How much of them are actually duplicated, and how much can we delete them? I think a lot of files can be removed.
I recently added an extremely heavy sanity check to the tycker, and it's causing some OOM on my laptop when running tests. These checks are removed in release builds, but we still want the tests to run faster.
From CLI args? From a file? Wdyt?
Commit: 708d533
universe u v
def test (A : Type u) (B : Type v) : Type (lmax u v) => A
Error message:
In file code/test.aya:48:48 ->
46 |
47 | universe u v
48 | def test (A : Type u) (B : Type v) : Type (lmax u v) => A
^-^
Error: Expected level expression, got: u v
Commit: beca413
open data Bool : Set | true | false
struct BoolPair : Set
| fst : Bool
| snd : Bool
open data U2 (x : BoolPair) : Set
| (false, false) => zero
| (false, true) => one
| (true, false) => two
| (true, true) => three
def not2 (x : BoolPair) : BoolPair
| (false, false) => (true, true)
| (false, true) => (true, false)
| (true, false) => (false, true)
| (true, true) => (false, false)
Both the data and the function definition cause the exception.
I don't really know the syntax for pattern matching on structs, so I could only guess it's the same as tuples as in Arend. Replace the parentheses with braces and the issue still occurs.
Judging from the source code, tycking for tuple patterns is not yet completed?
We could start from 'pattern definitions':
\def addN (a, b : Nat) : Nat
| zero, a => a
| a, zero => a
| suc a, b => suc (addN a b)
| a, suc b => suc (addN a b)
\pat one : Nat => suc zero
\pat suc-suc-a (a : Nat) => addN (suc (suc zero)) a
\def a-2 (a : Nat) : Nat
| suc-suc-a a => a
| one => one
| zero => zero
Note that I want to use \pat definitions as both patterns and functions.
Originally posted by @ice1000 in https://github.com/ice1000/aya-prover/issues/190#issuecomment-809092666
We are currently suffering from the following projects:
Also, I propose removing the tgbot subproject since it's useless.
This code tycks in beca413 but not in the latest build 5b7bfe3:
prim I
prim left
prim right
prim arcoe
struct Path (A : I -> Type) (a : A left) (b : A right) : Type
| at (i : I) : A i {
| left => a
| right => b
}
def path {A : I -> Type} (p : Pi (i : I) -> A i)
=> new Path A (p left) (p right) { | at i => p i }
def `=` Eq {A : Type} (a b : A) : Type => Path (\ i => A) a b
def idp {A : Type} (a : A) : a = a => path (\ i => a)
bind application tighter =
open data Unit : Set | unit
struct Struct : Set
| value : Unit
def getValue (t : Struct) : Unit => t.value
def setValue (x : Unit) (t : Struct) : Struct
=> new Struct { | value => x }
def value-inv : Pi {t : Struct} {u : Unit} -> u = getValue (setValue u t)
=> \{t} {u} => idp u
def foo {A : Set}
(get : Struct -> A)
(set : A -> Struct -> Struct)
(inv : Pi {t : Struct} {u : A} -> u = get (set u t))
=> unit
def bar : Unit => foo getValue setValue value-inv
(Want a better title for this issue)
Commit: 1707136
open data Unit : Set | unit
def foo : Pi {x : Unit} -> Unit => \{x} => x
def foo' : Pi {x : Unit} -> Unit => foo
Update:
@re-xyr The real use case is much more complex and the return type does depend on the implicit argument:
-- *** Prelude
prim I
prim left
prim right
prim arcoe
struct Path (A : I -> Type) (a : A left) (b : A right) : ooType
| at (i : I) : A i {
| left => a
| right => b
}
def path {A : I -> Type} (p : Pi (i : I) -> A i)
=> new Path A (p left) (p right) { | at i => p i }
def `=` Eq {A : Type} (a b : A) : ooType => Path (\ i => A) a b
def idp {A : Type} (a : A) : a = a => path (\ i => a)
def coe {a b : Type} (eq : a = b) (x : a) (i : I) : eq.at i
=> arcoe eq.at x i
bind = looser application
open data Unit : Set 0 | unit
-- *** Types
struct EventT : Set 1
| agentT : Set 0
def getAgentT (t : EventT) : Set 0 => t.agentT
def setAgentT (x : Set 0) (t : EventT) : EventT
=> new EventT { | agentT => x }
def agentT-inv (t : EventT) (u : Set 0) : u = getAgentT (setAgentT u t)
=> idp u
struct Event (t : EventT) : Set 2
| agent : t.agentT
def getAgent (t : EventT) (e : Event t) : t.agentT => e.agent
def Theta (setT : Set 0 -> EventT -> EventT) : ooType 4
=> Pi {u : Set 0} {t : EventT}
-> ((u -> ooType 3) -> ooType 3)
-> ((Event (setT u t) -> ooType 3) -> ooType 3)
-> (Event (setT u t) -> ooType 3) -> ooType 3
def mkTheta
(getT : EventT -> Set 0)
(get : Pi (t : EventT) -> Event t -> getT t)
(setT : Set 0 -> EventT -> EventT)
(invariant : Pi (t : EventT) (u : Set 0) -> u = getT (setT u t))
: Theta setT
=> \{u} {t} => \q p => \f =>
q (\x => p (\e =>
Sig (get (setT u t) e = coe (invariant t u) x right) ** (f e)))
def agent : Theta setAgentT
=> mkTheta getAgentT getAgent setAgentT agentT-inv
I had to change agent into \{u} {t} => mkTheta getAgentT getAgent setAgentT agentT-inv {u} {t} to make it type check.
I simplified it too much, sorry.
Commit: c7d7714
open data Unit : Type | unit
def foo (x : Unit) : Unit => x
def bar : Unit => foo {unit}
Expected behavior: type error
As title.
Currently, if you write (A B : Type), it is translated into (A : Type) (B : Type) right in the parser. This convenients the rest of the passes, but it makes the type term checked multiple times. If we can make it checked only once, that will save some heat produced by tycking, saving the world from global warming.
To do so, we need to change at least the concrete syntax, but not necessarily the core syntax.
This also applies to lambda terms.
Currently they're impled badly
Commit: 8d1e09d
universe l m
def Foo (A : Type l) : Type (lsuc (lmax l m)) => (A -> Type m) -> Type m
Basically,
implicit2.aya:
open data Unit : Set | unit
def y : Pi {a : Unit} -> Unit => \{a} => a
def x : Pi {a : Unit} -> Unit => y
def z : Pi {a : Unit} -> Unit => x
It does not typecheck as expected.
But a slightly different version causes NPE
open data Unit : Set | unit
def x : Pi {a : Unit} -> Unit => y
def y : Pi {a : Unit} -> Unit => \{a} => a
def z : Pi {a : Unit} -> Unit => x
stacktrace:
java.lang.NullPointerException
at java.base/java.util.Objects.requireNonNull(Objects.java:208)
at org.aya.core.def.Def.defLevels(Def.java:39)
at org.aya.tyck.ExprTycker.levelStuffs(ExprTycker.java:277)
at org.aya.tyck.ExprTycker.defCall(ExprTycker.java:265)
at org.aya.tyck.ExprTycker.inferRef(ExprTycker.java:231)
at org.aya.tyck.ExprTycker.doVisitRef(ExprTycker.java:223)
at org.aya.tyck.ExprTycker.visitRef(ExprTycker.java:212)
at org.aya.tyck.ExprTycker.visitRef(ExprTycker.java:57)
at org.aya.concrete.Expr$RefExpr.doAccept(Expr.java:244)
at org.aya.concrete.Expr.accept(Expr.java:41)
at org.aya.tyck.ExprTycker.checkNoZonk(ExprTycker.java:125)
at org.aya.tyck.ExprTycker.lambda$checkNoZonk$2(ExprTycker.java:123)
at org.aya.tyck.LocalCtx.with(LocalCtx.java:62)
at org.aya.tyck.LocalCtx.with(LocalCtx.java:47)
at org.aya.tyck.ExprTycker.checkNoZonk(ExprTycker.java:122)
at org.aya.tyck.ExprTycker.checkExpr(ExprTycker.java:135)
at org.aya.tyck.StmtTycker.lambda$visitFn$8(StmtTycker.java:184)
at kala.control.Either$Left.map(Either.java:166)
at org.aya.tyck.StmtTycker.visitFn(StmtTycker.java:183)
at org.aya.tyck.StmtTycker.visitFn(StmtTycker.java:43)
at org.aya.concrete.stmt.Decl$FnDecl.doAccept(Decl.java:324)
at org.aya.concrete.stmt.Decl.accept(Decl.java:70)
at org.aya.concrete.stmt.Decl.tyck(Decl.java:61)
at org.aya.concrete.resolve.module.FileModuleLoader.tyckModule(FileModuleLoader.java:99)
at org.aya.cli.single.SingleFileCompiler.compile(SingleFileCompiler.java:51)
at org.aya.test.TestRunner.runFile(TestRunner.java:66)
at org.aya.test.TestRunner.lambda$runDir$2(TestRunner.java:55)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.accept(ForEachOps.java:183)
at java.base/java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:179)
at java.base/java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:179)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.Iterator.forEachRemaining(Iterator.java:133)
at java.base/java.util.Spliterators$IteratorSpliterator.forEachRemaining(Spliterators.java:1845)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base/java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:150)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:173)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:596)
at org.aya.test.TestRunner.runDir(TestRunner.java:55)
at org.aya.test.TestRunner.runAllAyaTests(TestRunner.java:44)
Commit: 9984090
I'm trying to define mkVerb T p : Verb T:
universe u v
open data EventT : Type (lsuc u)
| CarrierT (A : Type u)
def GetAgentT (T : EventT {universe u}) : Type u
| CarrierT A => A
struct Event (T : EventT {universe u}) : Type u
| agent : GetAgentT T
def Quantifier (A : Type u) : Type (lmax u (lsuc v)) => (A -> Type v) -> Type v
def Verb (T : EventT {universe u}) : Type (lmax u (lsuc v))
=> Quantifier {universe u, v} (Event T)
def mkVerb {T : EventT {universe u}} (p : Event {universe u} T -> Type v)
: Verb {universe u, v} T
=> \f => Sig (e : Event {universe u} T) (s : p e) ** (f e)
And Aya required that Event.u <= Verb.v:
17 | def mkVerb {T : EventT {universe u}} (p : Event {universe u} T -> Type v)
18 | : Verb {universe u, v} T
^-------------^ Verb.u == u, Verb.v == v
19 | => \f => Sig (e : Event {universe u} T) (s : p e) ** (f e)
^------------------^ Event.u <= Verb.v
So I changed the definition of mkVerb:
def mkVerb {T : EventT {universe u}} (p : Event {universe u} T -> Type (lmax u v))
: Verb {universe u, lmax u v} T
=> \f => Sig (e : Event {universe u} T) (s : p e) ** (f e)
It's obvious that u <= lmax u v, but it still doesn't work.
Aya version: latest build (e4948a9) from GitHub Actions
Code:
def f {t : Set} : t -> (((t -> Set) -> Set) -> Set) -> Set
=> \x => \f => f (\g => g x)
Got warning:
In file code/test.aya:1:24 ->
1 | def f {t : Set} : t -> (((t -> Set) -> Set) -> Set) -> Set
^-----------------^
2 | => \x => \f => f (\g => g x)
Warning: The newly bound name `x5` shadows a previous local definition from outer scope
TODOs:
Aya version: latest build (0443f16) from GitHub Actions
Code:
data Entity : Set
| john
struct EventT : Set
| agentT : Set
struct Event (t : EventT) : Set
| agent : t.agentT
data Run (e : Event (new EventT { | agentT => Entity })) : Set
| (john) => run1
def mkVerb {t : EventT} (p : Event t -> Set) : (Event t -> Set) -> Set
=> \f => Sig (e : Event t) ** (Sig (p e) ** (f e))
How do we design pragmas? This is needed for the design of prelude.
--def f : Type 1 => Type 0
This should be very simple
fields that have default values are called FieldImpl in Aya source code.
Are we going to allow overwriting the field impls? for example
\struct Cross : \Set
| base : Nat
| plus1 => suc base
The plus1 has a value which depends on base. So we can use this syntax to create Cross:
\new Cross { | base => zero }
where the plus1 should be suc zero
Should we allow this new operation ?
\new Cross { | base => zero | plus1 => zero }
I think we should because we will have extends in the future which also overwrites fields.
What do you think?
How to do this? In Lean, if structure a extends b, then we can build a by either { to_b := some_b_instance, <fields of a> } or { <fields of b>, <fields of a> }. When accessing some b field in an a instance, we can either use a.field or a.to_b.field.
Say in type class resolution, we meet the following instance
instance FTrans {A B C} {{ab: F A B}} {{bc: F B C}} : F A C
and we have the resolution problem F X Y. In the description of the tabled typeclass resolution paper, it will generate two subgoals on this instance: F X ?M and F ?M Y.
However the ?M does not behave exactly like a metavariable. Namely, it can have multiple temporary [worse, may be not temporary because both solutions may be applicable to the remaining subgoal] solutions: if we have instances F X Z1 and F X Z2, then ?M equates to both in the resolution process.
Should we change how our metavariable works? Or should we use another kind of syntactic construct for this purpose?
Anybody wanna read some papers with me?
Plans:
Code:
prim I
prim left
prim right
struct Path (A : I -> Type) (a : A left) (b : A right) : Type
| at (i : I) : A i {
| left => a
| right => b
}
def path {A : I -> Type} (p : Pi (i : I) -> A i)
=> new Path A (p left) (p right) { | at i => p i }
def `=` Eq {A : Type} (a b : A) : Type => Path (\ i => A) a b
bind = looser application
def psqueeze {A : Type} {a a' : A} (p : a = a') (i : I) : a = p.at i => path (\j => p.at (I.squeeze i j))
Error:
In file test.aya:14:90 ->
12 | bind = looser application
13 |
14 | def psqueeze {A : Type} {a a' : A} (p : a = a') (i : I) : a = p.at i => path (\j => p.at (I.squeeze i j))
^^
Error: Expected type: Type
Normalized: Type
Want: struct type
Because we want to type a term such as: I
In file test.aya:14:90 ->
12 | bind = looser application
13 |
14 | def psqueeze {A : Type} {a a' : A} (p : a = a') (i : I) : a = p.at i => path (\j => p.at (I.squeeze i j))
^---------^
Error: Expected type: Type
Normalized: Type
Want: pi type
Because we want to type a term such as: I.squeeze i
In file test.aya:14:90 ->
12 | bind = looser application
13 |
14 | def psqueeze {A : Type} {a a' : A} (p : a = a') (i : I) : a = p.at i => path (\j => p.at (I.squeeze i j))
^-----------^
Error: Expected type: Type
Normalized: Type
Want: pi type
Because we want to type a term such as: I.squeeze i j
In file test.aya:14:72 ->
12 | bind = looser application
13 |
14 | def psqueeze {A : Type} {a a' : A} (p : a = a') (i : I) : a = p.at i => path (\j => p.at (I.squeeze i j))
^------------------------------^
Error: Expected type: Eq {A} a (p.at i)
Normalized: Path (λ i ⇒ A) a (p.at i)
Actual type: Path (λ _9 ⇒ A _9) (p.at <I.squeeze i j>) (p.at <I.squeeze i
j>)
Normalized: Path (λ _9 ⇒ A) (p.at <I.squeeze i j>) (p.at <I.squeeze i j>)
They don't match, sorry
🔨
Probably we only want the first error to appear.
Commit: f3b10ad
I'm trying to define Verb T = Quantifier (Event T).
(Why is the order of Quantifier's level params v, u, rather than u, v?)
universe u v
open data EventT : Type (lsuc u)
| CarrierT (A : Type u)
def GetAgentT (T : EventT {universe u}) : Type u
| CarrierT A => A
struct Event (T : EventT {universe u}) : Type u
| agent : GetAgentT T
def Quantifier (A : Type u) : Type (lmax u (lsuc v)) => (A -> Type v) -> Type v
def Verb (T : EventT {universe u}) : Type (lmax u (lsuc v)) => Quantifier {universe v, u} (Event T)
I plan to post all level related issues here in the future.
Commit: d2ef653
universe u
open data EventT : Type (lsuc u)
| CarrierT (A : Type u)
def GetAgentT (T : EventT) : Type u
| CarrierT A => A
struct Event (T : EventT) : Type (lsuc (lsuc u))
| agent : GetAgentT T
universe v
def Quantifier (A : Type u) : Type (lmax u (lsuc v)) => (A -> Type v) -> Type v
def Verb (T : EventT) : Type (lsuc (lsuc u)) => Quantifier (Event T)
def mkVerb {T : EventT} (p : Event T -> Type v) : Verb T
=> \f => Sig (e : Event T) (s : p e) ** (f e)
(Apart from the level error, it's strange that the level parameter (lsuc (lsuc u)) of the type of Event can be omitted)
(I'm trying to make the program I wrote before level-polymorphic)
(Would there be a way to specify the level parameters for functions manully?)
Aya version: latest build (e4948a9) from GitHub Actions
Code:
struct TypeStruct : Set
| type : Set
def setType (type' : Set) (ts : TypeStruct) : TypeStruct
=> new TypeStruct { | type => type' }
Got error:
In file code/test.aya:5:9 ->
3 |
4 | def setType (type' : Set) (ts : TypeStruct) : TypeStruct
5 | => new TypeStruct { | type => type' }
^--------------------------------^ TypeStruct.u <= TypeStruct.u
Error: Cannot solve some level equation(s)
There seems no way to solve this error.
PS. Will there be a syntax for struct updating like in Idris?
PS2. Will there be partial implementation like in Arend?
PS3. Do my issues feel spamming?
React
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
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
Django
The Web framework for perfectionists with deadlines.
Laravel
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.
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft
Open source projects and samples from Microsoft.
Google
Google ❤️ Open Source for everyone.
Alibaba
Alibaba Open Source for everyone
D3
Data-Driven Documents codes.
Tencent
China tencent open source team.