AlgebraicJulia / AlgebraicJulia/GATlab.jl

Symbolic constructs

Aberta
#80 1 comentário 0 reações 1 responsável Reivindicada por @olynch Ver no GitHub
infrastructure
Linguagem predominante
Julia
Estrelas
43
Forks
4
Métricas de merge de PRs
Nenhum PR com merge em 30d

Descrição

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).

Guia de contribuição

Nenhum guia de contribuição indexado para este repositório

Avaliação

Esta issue ainda não foi avaliada.

Receba novas issues na sua caixa de entrada

Um resumo curto de issues do GitHub para quem está começando.