AlgebraicJulia / AlgebraicJulia/GATlab.jl

Symbolic constructs

Ouverte
#80 1 commentaire 0 réactions 1 personne assignée Réclamée par @olynch Voir sur GitHub
infrastructure
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.

Recevez les nouvelles issues par e-mail

Un résumé court des issues GitHub adaptées aux débutants.