Repository navigation
Parte III Triad Full
Questa parte descrive il linguaggio definito da SPEC.md. Non è ancora
eseguibile dal runtime attuale: serve per conoscere lo standard, scrivere codice pronto per
S1 e capire i golden di conformance/cases/. Ogni capitolo indica la sezione di SPEC da cui
deriva. Gli output marcati Output (golden Full): provengono dai golden congelati.
Full estende il lessico di Core con:
| elemento | forma | esempi |
|---|---|---|
| identificatore | come Core, anche lettere non ASCII; ! finale se non seguito da =
|
età, push!
|
| variabile logica |
? attaccato a un nome |
?x, ?who
|
| variabile anonima |
?_ (ogni occorrenza è nuova) |
parent(?x, ?_) |
Float |
3.14, 1e-9
|
|
| interpolazione |
"x = $x", "$(a + b)"; escape aggiuntivo \$
|
|
| commenti annidati | #= a #= b =# c =# |
|
| macro | @nome(...) |
@unless(c, e) |
Parole chiave: function struct macro end if elseif else for in while let begin return break continue fact rule solve quote try catch with requires ensures true false nothing isa is.
Contestuali dopo solve: limit depth steps trace.
Regole dei due punti :
-
1:n,xs[2:end]::attaccato a un valore, senza spazi → range; -
f(:a),x = :a::non preceduto da un valore e seguito da un nome → simbolo; -
:( … )→ codice quotato; -
c ? a : b::circondato da spazi → ternario.
Regola del ?: ?x attaccato = variabile logica; ? con spazio = ternario.
Gli a capo chiudono un'istruzione, tranne dentro ( ), [ ] e :( ), e subito dopo un
operatore binario o una virgola di rule.
Tipi Full (oltre a quelli di Core):
| tipo | valori |
|---|---|
Int, Float (sottotipi di Number) |
42, 3.5
|
Expr |
codice quotato (Node) |
Term, Cons
|
termini e pattern lista logici |
Solution |
{who = :dave} |
Err |
errore come dato |
Type |
typeof(3) == Int |
| struct utente | Point(3.0, 4.0) |
Any |
supertipo di tutto, usato nelle firme |
Variabili tipate:
x::Int = 5
x = 6 # bene
x = 5.5 # Err(:type): il nome mantiene il tipo dichiarato
y::Float = 1.0
y = 2 # 2.0: conversione Int → FloatIl vincolo nasce con la dichiarazione e vive nell'ambiente in cui il nome è stato creato.
sq(x) = x * x
area(n::Number) = :number
area(n::Int) = :int
function dist(a::Point, b::Point)::Float
requires a.x != b.x || a.y != b.y
sqrt((a.x - b.x)^2 + (a.y - b.y)^2)
end
function +(a::Point, b::Point) # gli operatori sono funzioni ridefinibili
Point(a.x + b.x, a.y + b.y)
endRegole:
- vince il metodo più specifico tra gli applicabili (
area(1) == :int,area(1.5) == :number); - nessun metodo applicabile →
Err(:method)(o fallback builtin per gli operatori numerici); - più metodi ugualmente specifici →
Err(:ambiguous); - il tipo di ritorno
::Rè controllato all'uscita (con conversione Int→Float); - funzioni e operatori sono valori:
reduce(+, xs),map(sq, xs); - lambda tipate:
function (x::Int) x end→f(2.0)èErr(:type).
struct Point
x::Float
y::Float
end
p = Point(3, 4) # costruttore posizionale, Int → Float
p.x # 3.0
typeof(p) == Point # true
p isa Point # true- Immutabili; campi tipizzati.
- Campo inesistente →
Err(:field); tipo sbagliato →Err(:type). - In Core lo stesso concetto si rappresenta con una lista taggata (§16.2).
s = 0
for i in 1:10
s += i
end # s == 55
xs = [1, 2, 3]
xs[end] # 3
xs[2:end] # [2, 3]
[x^2 for x in 1:4 if x > 2] # [9, 16]
x = 3; x > 2 ? :big : :small # :big
e = try div(1, 0) end # l'errore diventa il valore
r = try div(1, 0) catch err; 0 end # con catch: err è l'Err, il valore è quello del ramoAltri valori attesi (dai vecchi test dell'implementazione Julia):
x = 2; y = x * 21; y # 42
7 / 2 # 3.5
"ab" * "cd" # "abcd"
let a = 1, b = a + 1; a + b; end # 3
if 1 > 2; :a; elseif 2 > 1; :b; else; :c; end # :b
sq(x) = x * x; map(sq, [1, 2, 3]) # [1, 4, 9]
reduce(+, [1, 2, 3, 4]) # 10
filter(x -> x % 2 == 0, 1:6) # [2, 4, 6]
function fact_(n::Int)::Int
if n <= 1; return 1; end
n * fact_(n - 1)
end; fact_(10) # 3628800requires c al top level è un'asserzione; ensures c è ammesso solo dentro function.
fact parent(:alice, :bob)
fact parent(:alice, :carol)
fact parent(:bob, :dave)
rule grandparent(?x, ?z) :- parent(?x, ?y), parent(?y, ?z)
rule ancestor(?a, ?d) :- parent(?a, ?d)
rule ancestor(?a, ?d) :- parent(?a, ?x), ancestor(?x, ?d)solve restituisce una lista di Solution (è un valore, non stampa nulla):
sols = solve grandparent(:alice, ?who) limit 5
[s.who for s in sols] # [:dave]
[s.d for s in solve ancestor(:alice, ?d)]- Opzioni:
limit n,depth d,steps s(default 1 000 000),trace. - Un predicato usato come funzione è un
Bool:grandparent(:alice, :dave)→true; si può usare inif. - Goal:
p(t…),g1 && g2,(g1, g2),g1 || g2,!g/not(g),a = b(unificazione),?y is espr, confronti, funzione Triad che restituisceBool,true/false. - Occurs-check attivo:
solve ?x = f(?x)non ha soluzioni (non va in ciclo). - Liste stile Prolog nei pattern:
[?h | ?t]. -
vars(s)restituisce i nomi legati in unaSolution; si accede cons.nomeos[:nome].
Esempi:
# percorso con costo
fact edge(:a, :b, 2)
fact edge(:b, :c, 3)
rule path(?x, ?y, ?c) :- edge(?x, ?y, ?c)
rule path(?x, ?y, ?c) :- edge(?x, ?z, ?c1), path(?z, ?y, ?c2), ?c is ?c1 + ?c2
(solve path(:a, :c, ?costo))[1].costo # 5
# append alla Prolog
rule app([], ?l, ?l)
rule app([?h | ?t], ?l, [?h | ?r]) :- app(?t, ?l, ?r)
(solve app([1, 2], [3], ?r))[1].r # [1, 2, 3]
length(solve app(?a, ?b, [1, 2, 3])) # 4
# negazione per fallimento
fact parent(:tom, :bob)
persone = [:tom, :bob]
foglie = filter(p -> !parent(p, ?_), persone) # [:bob]Pattern di lista con arità esatta; le parentesi attorno al pattern sono obbligatorie.
(a, b) = [1, 2] # a == 1, b == 2
e = try (a, b) = [1] end # e.kind == :bounds
e = try (a, b) = [1, 2, 3] end # e.kind == :bounds
xs = []
for (k, v) in [[1, 2], [3, 4]]
push!(xs, k + v)
end # xs == [3, 7]- Un elemento non lista o di arità diversa nel
for→Err(:bounds)oErr(:type). -
function f((a, b))definisce due parametriaeb(i parametri sono appiattiti):f(10, 20) == 30. Per destrutturare un singolo argomento lista usa(a, b) = pairnel corpo. - I pattern annidati ricorsivi non sono ancora previsti.
Un errore è un valore Err(kind, msg, data); non diventa un'eccezione dell'host salvo che non
sia gestito al top level (allora il processo esce con codice 1 e stdout vuoto per l'istruzione
fallita: è il caso di conformance errore).
e = try div(1, 0) end # Err(:domain, ...)
e.kind # :domain
e.msg # messaggio
iserr(e) # true
7.0 / 0 # Inf: la divisione Float non è un errore
throw(err(:mio, "ops", 42))
error("boom") # Err(:error, ...)
describe(e::Err) = string("errore ", e.kind, ": ", e.msg)
describe(x::Any) = string("valore ", x)
for r in [try div(10, d) end for d in [2, 0, 5]]
println(describe(r))
endKinds standard: :syntax, :undef, :type, :method, :ambiguous, :field, :bounds,
:domain, :instantiation, :contract, :budget, :effect, :host.
Err(:syntax) porta in data la posizione (e.data.line, e.data.col).
function safe_div(a::Number, b::Number)::Float
requires b != 0
ensures abs(result * b - a) < 1e-9
a / b
end
safe_div(6, 3) # 2.0
e = try safe_div(1, 0) end
e.kind # :contract
e.data.clause # :requires
e.data.fn # :safe_div-
requires cè controllata dove compare (inizio del corpo, oppure al top level come asserzione). -
ensures cè controllata all'uscita, conresultlegato al valore restituito, dopo il controllo del tipo di ritorno. - Violazione →
Err(:contract, …)condata.clause,data.fn,data.cond,data.result. - I contratti sono puri: un effetto dentro un contratto →
Err(:effect). -
ensuresfuori dafunction→Err(:syntax).
r = with budget(steps = 10_000)
while true end
end
r.kind # :budget — il ciclo infinito diventa un valore- Un passo = una chiamata, un'iterazione di ciclo, un passo di risoluzione.
- I budget si annidano: vale il più stretto; solo il budget del
withcorrente diventa valore, quello esterno si propaga. -
solve … steps Nè il budget di una singola query. - La ricorsione infinita non fa stack overflow: finisce in
Err(:budget)(stack esplicito).
La traccia è un valore, non output.
fib(n::Int) = n < 2 ? n : fib(n - 1) + fib(n - 2)
t = with trace
fib(3)
end
t.result # 2
t.trace # [Event(port=:call, fn=:fib, args=[3], depth=0), …]
t = solve path(:a, :c) trace
t.trace # porte Byrd: :call, :exit, :redo, :fail, :depthGli eventi sono record con port, goal/fn, depth (e value/args per le funzioni):
si filtrano come qualsiasi valore.
Le funzioni sono pure per default. Effetti: io (println, print) e state (fact/rule
dentro una funzione).
function saluta(nome::String) !io
println("ciao, ", nome)
end
function impara(x) !state
fact visto($x)
end- Controllo dinamico: una funzione pura che chiama una
!iooprintln→Err(:effect). - Il top level permette tutti gli effetti; le lambda ereditano quelli del contesto.
- Macro e contratti sono puri; leggere la KB (
solve, predicati) è puro. - Mutare liste o variabili locali non è un effetto.
Il parser produce un solo tipo di nodo, Node(head, args): è lo stesso albero che il kernel
esegue, che :( … ) restituisce e che --tree stampa come S-expression.
| sintassi | nodo |
|---|---|
f(a, b), a + b
|
(call f a b), (call + a b)
|
a && b, a || b
|
(and a b), (or a b)
|
x = e |
(assign x e) |
:alice |
(sym alice) |
a.x, xs[i]
|
(dot a x), (index xs i)
|
[a, b], [h | t]
|
(list a b), (cons (list h) t)
|
[e for x in xs if c] |
(comprehension e x xs c) |
x -> e |
(lambda (tuple x) e) |
x::T |
(typed x T) |
"a $x" |
(string "a " x) |
if c a else b end, c ? a : b
|
(if c (block a) (block b)) |
while, for, let, begin
|
(while c body), (for x iter body), (let (tuple …) body), (block …)
|
function f(a::T)::R !io … end |
(function f (tuple (typed a T)) R (tuple io) body) |
struct P; x::Float; end |
(struct P (tuple (typed x Float))) |
macro m(a) … end, @m(e)
|
(macro m (tuple a) body), (macrocall m e)
|
:(e), quote … end, $e
|
(quasi e), (quasi (block …)), (unquote e)
|
fact t, rule h :- g1, g2
|
(fact t), (rule h g1 g2)
|
solve g limit 5 trace |
(solve g (tuple (assign limit 5) (assign trace true))) |
try b catch e h end |
(try b e h) |
with budget(steps = N), trace … end |
(with (tuple (call budget (assign steps N)) trace) body) |
c = :(a.x + f(b, 2))
c.head # :call
sexpr(c) # "(call + (dot a x) (call f b 2))"
n = 7
quadrato = :($n * $n)
eval(quadrato) # 49
parse("if x > 0; :pos; else; :neg; end") # albero
unparse(parse_program("1:n")) # "1:n"
Expr(:call, :f, 1) # costruisce un NodeLe macro ricevono codice e restituiscono codice; l'espansione è pura e non igienica:
usa gensym() per nomi freschi.
macro unless(c, body)
:(if !$c; $body; end)
end
macro swap(a, b)
tmp = gensym(:tmp)
quote
$tmp = $a
$a = $b
$b = $tmp
end
end
macro time_it(label, e)
:(begin
r = $e
println($label, " -> ", r)
r
end)
end
@swap(x, y)
@unless(x < y, println("x non è minore di y"))
@time_it("somma", reduce(+, 1:100)) # stampa "somma -> 5050"function poly(coeffs)
acc = :(0)
i = 0
for c in coeffs
acc = :($acc + $c * x ^ $i)
i += 1
end
acc
end
p = poly([1, 2, 3])
x = 2
eval(p) # 17| ambito | funzioni |
|---|---|
| aritmetica e confronto |
+ - * / ^ % == != < <= > >= !, abs sqrt floor ceil round exp log sin cos div mod min max; * concatena stringhe |
| liste |
length isempty first last rest reverse sort sum push! pop! append! vcat collect, a:b, x in xs
|
| ordine superiore | map filter reduce any all count |
| stringhe e output | string repr println print |
| tipi |
typeof, isa, Int Float String Symbol
|
| errori | err iserr throw error |
| codice | eval parse unparse sexpr Expr gensym |
| logica | vars(sol) |
Di questi, Core fornisce solo + - * % ^, confronti, && || !, length, push!, indicizzazione,
* su stringhe, Int, string, Symbol, print, println, typeof (SPEC-CORE §7).
Interfaccia normativa di triad (oggi il runtime implementa solo triad FILE [ARG...] e,
nell'interprete JS, triad -):
triad # REPL
triad FILE [ARG...] # esegue FILE; ARGS == [ARG...]
triad -l FILE # carica FILE e apre il REPL
triad -i FILE # esegue FILE e poi apre il REPL
triad -e CODE # esegue CODE
triad -E CODE # esegue CODE e stampa il valore
triad --tree FILE # stampa l'albero uniforme come S-expression
triad -q # REPL senza banner
triad -h, --help
triad -v, --version
triad - # legge lo script da stdin
- L'estensione
.triad/.tdsi può omettere; lo shebang#!è ignorato. - Exit:
0successo,1errore non gestito (stampato su stderr),2uso non valido.
REPL (stile Prolog):
triad> 1 + 2
3
triad> ?- ancestor(:tom, ?d)
?d = :bob ;
?d = :liz.
triad> parent(:jim, ?x)
false.
- I blocchi aperti restano in attesa fino a
end. -
?- goal(o un goal su un predicato della KB) esegue una query; dopo ogni soluzione;/n/spazio = successiva,a= tutte, invio/.= stop. - Comandi:
:load FILE…(:l),:reload(:r,make),:listing [nome|nome/arità](:ls),:tree CODICE,:reset,:help(:h),:quit(:q,halt, Ctrl-D).
I file sono in examples/ (eseguibili quando S1 sarà pronto); gli output sono i golden
congelati in conformance/cases/.
| file | copre | caso golden |
|---|---|---|
examples/assaggio.td |
struct, dispatch, logica, macro, contratti | assaggio |
examples/famiglia.td |
fatti/regole, ricorsione, liste Prolog, negazione | famiglia |
examples/garanzie.td |
errori, contratti, budget, tracce, effetti | garanzie_core |
examples/macro.td |
quote, eval, macro, gensym | macro |
examples/tour.td |
tutti i paradigmi | tour |
examples/hello_shebang.td |
shebang, ARGS, effetti |
hello_shebang |
examples/benvenuto.triad |
estensione canonica, Float, solve
|
— |
struct Point
x::Float
y::Float
end
function dist(a::Point, b::Point)::Float
requires a.x != b.x || a.y != b.y
sqrt((a.x - b.x)^2 + (a.y - b.y)^2)
end
fact parent(:alice, :bob)
fact parent(:bob, :dave)
rule grandparent(?x, ?z) :- parent(?x, ?y), parent(?y, ?z)
result = solve grandparent(:alice, ?who) limit 5
println("nipoti: ", result) # [{who = :dave}]
println("primo: ", result[1].who) # :daveOutput (golden Full) del file completo:
nipoti di alice: [{who = :dave}]
primo: dave
quanti: 1
dist(p, q) = 5.0
dist(p, p) -> Err(:contract, "requires violata in dist: a.x != b.x || a.y != b.y", Info(fn = :dist, clause = :requires, cond = :(a.x != b.x || a.y != b.y)))
tipo: contract
almeno un nipote
alice è nonna di dave? true
Output (golden Full):
discendenti di tom: [:bob, :liz, :ann, :pat, :jim]
fratelli di ann: [:pat]
madri: ["pat -> jim"]
senza figli: [:liz, :ann, :jim]
over 50: [:tom, :bob]
modi di spezzare [1, 2, 3]:
[] ++ [1, 2, 3]
[1] ++ [2, 3]
[1, 2] ++ [3]
[1, 2, 3] ++ []
figli di bob: [:ann, :pat]
Output (golden Full, traccia abbreviata):
2.5
violazione: contract — requires violata in safe_div: b != 0
clausola: requires, funzione: safe_div
valore 5
errore domain: divisione intera per zero
valore 2
valore 42
errore input: età non valida
catturato mio con dati [1, 2, 3]
ciclo infinito -> budget
solve infinito -> budget
fib(3) = 2 in 10 eventi
chiamate: [[3], [2], [1], [0], [1]]
call path(:a, :c) @0
call edge(:a, :c) @1
fail edge(:a, :c) @1
…
ciao, Triad
effetto non dichiarato -> println richiede !io ma rumorosa non lo dichiara
imparato: [:gatto]
Output (golden Full):
codice: :(a.x + f(b, 2))
head: call
args: [:+, :(a.x), :(f(b, 2))]
sexpr: (call + (dot a x) (call f b 2))
:(7 * 7) = 49
parse: (if (call > x 0) (block (sym pos)) (block (sym neg)))
unparse: if x > 0; :pos; else; :neg; end
dopo @swap: x = 2, y = 1
x non è minore di y
somma -> 5050
polinomio: :(0 + 1 * x ^ 0 + 2 * x ^ 1 + 3 * x ^ 2)
p(2) = 17
function safe_div(a::Number, b::Number)::Float
requires b != 0
ensures abs(result * b - a) < 1e-9
a / b
end
e = try safe_div(1, 0) end
e.kind # :contract
r = with budget(steps = 1000)
while true end
end
r.kind # :budget← Parte II Triad Core · Home · Parte IV Codice del progetto →
Parte prima
Parte seconda 4. Le parole del linguaggio 5. Valori e tipi 6. Espressioni, operatori e variabili 7. Decidere e ripetere 8. Funzioni e ricorsione 9. Lambda, chiusure e visibilità dei nomi 10. Liste e dati strutturati 11. Stringhe, simboli e byte 12. Quando le cose vanno storte 13. Progetto: un piccolo interprete
Parte terza 14. Tipi, struct e multiple dispatch 15. Programmazione logica 16. Codice come dato e macro 17. Garanzie, costrutti Full e interfaccia
Parte quarta 18. Anatomia del progetto e contratto di conformità 19. L'interprete di riferimento 20. Il seed in codice macchina 21. Verso il self-hosting 22. Gli strumenti di sviluppo
Appendici
- Riferimento dei builtin Core
- Catalogo conformance Core
- Catalogo conformance Full
- Sorgenti degli esempi
- Sorgenti self-hosted
- Documenti di riferimento
- Indice analitico
Manuale di consultazione