Current section
Files
Jump to
Current section
Files
src/fluoresce.erl
-module(fluoresce).
-compile([no_auto_import, nowarn_unused_vars, nowarn_unused_function, nowarn_nomatch]).
-export([wrap/1, do/2, bind/2, join/1, co/2, disjunctive_syllogism/2, callcc/1, throw/2, excluded_middle/0, double_negate/1, adjunction/1, double_negation_elimination/1, contramap/2, implies/1, modus_ponens/2, de_morgan_1/1, de_morgan_2/1, de_morgan_3/1, de_morgan_4/1, function_to_coexponential/1, coexponential_to_function/1, pierces_law/1, main/0]).
-export_type([not_not/2]).
-type not_not(FQU, FQV) :: {cont, fun((fun((FQV) -> FQU)) -> FQU)}.
-spec compose(fun((FRD) -> FRE), fun((FRF) -> FRD)) -> fun((FRF) -> FRE).
compose(F, G) ->
fun(X) -> F(G(X)) end.
-spec wrap(FRG) -> not_not(any(), FRG).
wrap(A) ->
{cont, fun(K) -> K(A) end}.
-spec do(not_not(FRK, FRL), fun((FRL) -> FRO)) -> not_not(FRK, FRO).
do(C, F) ->
{cont, fun(K) -> (erlang:element(2, C))(fun(A) -> K(F(A)) end) end}.
-spec bind(not_not(FRR, FRS), fun((FRS) -> not_not(FRR, FRV))) -> not_not(FRR, FRV).
bind(C, F) ->
{cont,
fun(K) ->
(erlang:element(2, C))(fun(A) -> (erlang:element(2, F(A)))(K) end)
end}.
-spec join(not_not(FSA, not_not(FSA, FSB))) -> not_not(FSA, FSB).
join(A) ->
{cont,
fun(K) ->
(erlang:element(2, A))(fun(B) -> (erlang:element(2, B))(K) end)
end}.
-spec co(
fun((fun((FSJ) -> FSI)) -> not_not(FSI, FSM)),
fun(({ok, FSM} | {error, FSJ}) -> not_not(FSI, FSR))
) -> not_not(FSI, FSR).
co(F, Rest) ->
{cont,
fun(K) ->
K2 = fun(A) -> (erlang:element(2, Rest(A)))(K) end,
(erlang:element(
2,
F(compose(K2, fun(Field@0) -> {error, Field@0} end))
))(compose(K2, fun(Field@0) -> {ok, Field@0} end))
end}.
-spec disjunctive_syllogism(
not_not(FSW, {ok, FSX} | {error, FSY}),
fun((FSY) -> FSW)
) -> not_not(FSW, FSX).
disjunctive_syllogism(E, Not_a) ->
{cont, fun(K) -> (erlang:element(2, E))(fun(Res) -> case Res of
{error, A} ->
Not_a(A);
{ok, E@1} ->
K(E@1)
end end) end}.
-spec callcc(fun((fun((FTI) -> FTH)) -> FTI)) -> not_not(FTH, FTI).
callcc(F) ->
co(fun(K) -> wrap(F(K)) end, fun(S) -> _pipe = case S of
{error, A} ->
A;
{ok, A@1} ->
A@1
end,
wrap(_pipe) end).
-spec throw(FTN, fun((FTN) -> FTO)) -> not_not(FTO, any()).
throw(A, Not_a) ->
Instant_fail = wrap({error, A}),
disjunctive_syllogism(Instant_fail, Not_a).
-spec excluded_middle() -> not_not(FTU, {ok, fun((FTV) -> FTU)} | {error, FTV}).
excluded_middle() ->
co(fun(K) -> wrap(K) end, fun(Cofn) -> wrap(Cofn) end).
-spec double_negate(FUC) -> not_not(FUD, fun((fun((FUC) -> FUD)) -> FUD)).
double_negate(A) ->
bind(excluded_middle(), fun(Lem) -> case Lem of
{error, Not_a} ->
throw(A, Not_a);
{ok, Not_not_a} ->
wrap(Not_not_a)
end end).
-spec adjunction(fun((fun((FUL) -> FUK)) -> not_not(FUK, FUO))) -> not_not(FUK, fun((fun((FUO) -> FUK)) -> not_not(FUK, FUL))).
adjunction(F) ->
co(
fun(K) -> F(K) end,
fun(S) ->
T = wrap(case S of
{error, A} ->
{ok, A};
{ok, B} ->
{error, B}
end),
wrap(fun(Not_b) -> disjunctive_syllogism(T, Not_b) end)
end
).
-spec double_negation_elimination(fun((fun((FUY) -> FUX)) -> FUX)) -> not_not(FUX, FUY).
double_negation_elimination(Not_not_a) ->
bind(adjunction(fun(Not_a) -> wrap(Not_a) end), fun(F) -> F(Not_not_a) end).
-spec contramap(fun((FVG) -> FVF), fun((FVJ) -> not_not(FVF, FVG))) -> not_not(FVF, fun((FVJ) -> FVF)).
contramap(Not_b, F) ->
bind(
adjunction(
fun(Not_not_a) ->
bind(double_negation_elimination(Not_not_a), fun(A) -> F(A) end)
end
),
fun(F2) -> F2(Not_b) end
).
-spec implies(fun((FVQ) -> not_not(FVR, FVS))) -> not_not(FVR, {ok, FVS} |
{error, fun((FVQ) -> FVR)}).
implies(F) ->
co(
fun(Not_not_a) -> bind(double_negation_elimination(Not_not_a), F) end,
fun(S) -> wrap(S) end
).
-spec modus_ponens({ok, FWB} | {error, fun((FWD) -> FWC)}, FWD) -> not_not(FWC, FWB).
modus_ponens(F, A) ->
bind(
double_negate(A),
fun(Not_not_a) -> disjunctive_syllogism(wrap(F), Not_not_a) end
).
-spec de_morgan_1(fun(({ok, FWM} | {error, FWN}) -> FWL)) -> not_not(FWL, {fun((FWN) -> FWL),
fun((FWM) -> FWL)}).
de_morgan_1(X) ->
bind(
contramap(X, compose(fun wrap/1, fun(Field@0) -> {error, Field@0} end)),
fun(L) ->
bind(
contramap(
X,
compose(fun wrap/1, fun(Field@0) -> {ok, Field@0} end)
),
fun(R) -> wrap({L, R}) end
)
end
).
-spec de_morgan_2({fun((FWZ) -> FWY), fun((FXC) -> FWY)}) -> not_not(FWY, fun(({ok,
FXC} |
{error, FWZ}) -> FWY)).
de_morgan_2(X) ->
{Not_a, Not_b} = X,
contramap(Not_b, fun(A) -> disjunctive_syllogism(wrap(A), Not_a) end).
-spec de_morgan_3(fun(({FXM, FXN}) -> FXL)) -> not_not(FXL, {ok,
fun((FXN) -> FXL)} |
{error, fun((FXM) -> FXL)}).
de_morgan_3(X) ->
bind(
adjunction(
fun(Y) ->
bind(
de_morgan_1(Y),
fun(_use0) ->
{Not_not_a, Not_not_b} = _use0,
bind(
double_negation_elimination(Not_not_a),
fun(A) ->
bind(
double_negation_elimination(Not_not_b),
fun(B) -> wrap({A, B}) end
)
end
)
end
)
end
),
fun(F) -> F(X) end
).
-spec de_morgan_4({ok, fun((FXZ) -> FXY)} | {error, fun((FYC) -> FXY)}) -> not_not(FXY, fun(({FYC,
FXZ}) -> FXY)).
de_morgan_4(X) ->
bind(excluded_middle(), fun(Lem) -> case Lem of
{error, {A, B}} ->
case X of
{error, Not_a} ->
throw(A, Not_a);
{ok, Not_b} ->
throw(B, Not_b)
end;
{ok, Not_pair} ->
wrap(Not_pair)
end end).
-spec function_to_coexponential(fun((FYL) -> not_not(FYM, FYN))) -> not_not(FYM, fun(({FYL,
fun((FYN) -> FYM)}) -> FYM)).
function_to_coexponential(F) ->
bind(implies(F), fun(Or) -> case Or of
{error, Not_a} ->
de_morgan_4({error, Not_a});
{ok, B} ->
bind(
double_negate(B),
fun(Not_not_b) -> de_morgan_4({ok, Not_not_b}) end
)
end end).
-spec coexponential_to_function(fun(({FYY, fun((FYZ) -> FYX)}) -> FYX)) -> not_not(FYX, fun((FYY) -> not_not(FYX, FYZ))).
coexponential_to_function(C) ->
_pipe = fun(A) -> bind(de_morgan_3(C), fun(Or) -> case Or of
{error, Not_a} ->
throw(A, Not_a);
{ok, Not_not_b} ->
double_negation_elimination(Not_not_b)
end end) end,
wrap(_pipe).
-spec pierces_law(fun((fun((FZJ) -> not_not(FZK, any()))) -> not_not(FZK, FZJ))) -> not_not(FZK, FZJ).
pierces_law(F) ->
bind(implies(F), fun(Or) -> case Or of
{error, Not_a} ->
bind(
adjunction(fun coexponential_to_function/1),
fun(F@1) ->
do(
F@1(Not_a),
fun(_use0) ->
{Out, _} = _use0,
Out
end
)
end
);
{ok, A} ->
wrap(A)
end end).
-spec main() -> integer().
main() ->
gleam@io:println(<<"Hello from fluoresce!"/utf8>>),
G = (bind(
double_negate(3),
fun(Not_not_a) ->
bind(
callcc(fun(_) -> gleam@io:debug(<<"hi"/utf8>>) end),
fun(_) -> do(excluded_middle(), fun(Lem) -> case Lem of
{error, Not_a} ->
throw(Not_a, Not_not_a);
{ok, _} ->
double_negation_elimination(Not_not_a)
end end) end
)
end
)),
(erlang:element(2, G))(
fun(A) -> (erlang:element(2, A))(fun gleam@io:debug/1) end
).