AlgebraicJulia / AlgebraicJulia/GATlab.jl
Symbolic constructs
- Langage dominant
- Julia
- Étoiles
- 43
- Forks
- 4
- Métriques de merge des PR
- Aucune PR mergée en 30 j
Description
We should have a macro that makes writing symbolic functions as easy as writing normal functions. Something like
```julia
@symbolic(ThRing) function foo(a, b)
a^2 + b^2
end
```
should produce a symbolic function in the theory of rings out of the context `[a,b]`. Then symbolic functions should be able to be applied inside other symbolic functions, so we could have
```julia
@symbolic(ThRing) function bar(x,y,z)
foo(x,y) + foo(y,z)
end
```
Of course, this should support types, so that we have
```julia
@symbolic(ThModule) function interpolate(r::Scalar, v::Vector, w::Vector)::Vector
(1 - r) * v + r * w
end
```
This should extend to "symbolic structs".
```julia
@symbolic(ThRing) struct Pos2D
x
y
end
@symbolic(ThRing) function abs2(p::Pos2D)
foo(p.x, p.y)
end
```
Finally, we should support some sort of "comptime" abstraction, where symbolic functions can have parameters which are Julia values. Something like:
```julia
@symbolic(ThRing) function power(n::Int)(a)
acc = 1
for i in (@julia 1):n
acc = acc * a
end
acc
end
```
This would expand into a Julia function that looked something like
```julia
function power(n::Int)
_context = ...
_a = Trm(Lvl(1; context=true))
function _mul(x,y)
Trm(getlevel(ThRing.*), [x,y])
end
_1 = Trm(getlevel(ThRing.one), [])
acc = _1
for i in 1:n
acc = _mul(acc, _a)
end
TrmInContext(_context, acc)
end
```
I think this is a good design for how to work with #73. Of course, this takes us dangerously close to implementing Agda in Julia, but I think this actually shouldn't be *too* hard (famous last words).
Guide de contribution
Aucun guide de contribution indexé pour ce dépôt
Évaluation
Cette issue n'a pas encore été évaluée.