Skip to content

Instantly share code, notes, and snippets.

@L8D L8D/spec-zvi

Created Apr 2, 2015
What would you like to do?
% comments are like this
% outside of operator precedence, the only special
% syntax is ':-' and ':='. ':=' is used for a type
% annotation. Types are just additional predicate
% calls, but they are restricted to not using IO
% values or ambigious stuff a compiler couldn't
% figure out.
my_predicate := true. % my_predicate is valid under any pretense
my_predicate :- true. % my_predicate is true under any pretense
my_predicate. % same as above.
% when a signature is always true, you don't need
% to write it, it will be infered. This is common
% shorthand for declaring types. For example:
% data Nat = Zero | Succ Nat
nat(succ(N)) :- nat(N).
% data Ordering = Equal | Greater | Lesser
% now we can use ordering in a type declaration:
compare(X, Y, R) := A(X), A(Y), ordering(R). % a -> a -> Ordering
% because all types are of rank N, like the 'A'
% type predicate above, any number of implementations
% for any number of types of the predicate may be
% written.
% where A = nat (but really it's more that nat
% satisfies the type, any other type that uses
% zero and/or succ(_) as constructors are also
% valid implementations)
compare(zero, zero, equal).
compare(zero, succ(_), lesser).
compare(succ(_), zero, greater).
compare(succ(X), succ(Y), R) :- compare(X, Y, R).
% Zvi doesn't have *real* type classes, it just
% uses it's fancy rank types to declare type
% classes as synonyms for types that have
% implementations for abstract pedicates.
ord(A) := type(A). % A must be a valid type predicate.
ord(A) :- A(X), A(Y), compare(X, Y, _). % these X and Y values are
% just phantom types used to
% place restrictions on what
% types can satisfy ord(A).
% They don't exist anywhere else.
less(X, Y) := ord(A), A(X), A(Y).
less(X, Y) :- compare(X, Y, lesser).
map(P, X, Y) := pred(A, B, P), F(A, FofA), F(B, FofB), FofA(X), FofB(Y).
functor(F) := pred(type, type, F). % F must be a valid type constructor
functor(F) :- F(A, FofA), F(B, FofB), map(_, FofA, FofB).
pure(X, R) := A(X), F(A, FofA), FofA(R).
ap(FP, FX) := F(A, FofA), FofA(FX), F(B, FofB) % zzzZZzzZZz...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.