groupoid / henk.ex Goto Github PK
View Code? Open in Web Editor NEW🧊 Чиста система з всесвітами
Home Page: https://henk.groupoid.space
License: Other
🧊 Чиста система з всесвітами
Home Page: https://henk.groupoid.space
License: Other
And document a way to run it.
E.g \
, ->
, forall
$ cat intro
∀ (Intro:
(
∀ (a : A)
→ ∀ (aok : AOk a)
→ BOk (isoAB a)
)
→ ( ∀ (a1: A)
→ ∀ (a1ok : AOk a1)
→ ∀ (a2 : A)
→ ∀ (a2ok: AOk a2)
→ AEqu a1 a2
→ BEqu (isoAB a1) (isoAB a2)
)
→ AND)
→ AND
There is a workaround involving additional pair of brackets for Intro
type.
Copy-Paste for now is ok, but we need deeper understanding of AST enrichment through ordered blocks of stream parsers chained in one function-pipeline. This would be an Erlang prototype of the future Exe modular stream parser.
A term that looks much worse after normalization. E.g. the one that uses sharing extensively.
It is not a counterexample to normalization per se, but to normalization seen as optimization or god forbid superoptimization.
The issue was discussed in gitter.
Use a common error message format in both checker and parser, such as those of Erlang or GCC. Provision for long multi-line errors.
Requires #12
currently parser returns {0,0}
(what it should mean?) when file referenced does not exist.
expected behaviour: error with hash-reference file path and its position in source.
Files #Morte/recursive
and #Morte/corecursive
are inlined.
We need to uninline them to use #IO/Make
and #Maybe/maybe
FQN external files.
diff --git a/README.md b/README.md
index 1e0732a..e8f0d1d 100644
--- a/README.md
+++ b/README.md
@@ -5,7 +5,7 @@ Maxim Sokhatsky [email protected]
![Om](http://upload.wikimedia.org/wikipedia/commons/thumb/2/2a/Georg_Simon_Ohm3.jpg/200px-Georg_Simon_Ohm3.jpg)
-Georg Simon Ohm -- a German physicist and mathematician who was born in german town Erlangen.
+Georg Simon Ohm -- a German physicist and mathematician who was born in German town Erlangen.
Abstract
--------
@@ -47,7 +47,7 @@ from λ value-level functions.
Note than list/1 is special type constructor only for built-in Erlang list types.
All type constructors with zero arity denoted as concrete types. It has
-compatiblity with Erlang dializer syntax, e.g.:
+compatibility with Erlang dializer syntax, e.g.:
string() = list(char) = string/0.
integer().
@@ -69,7 +69,7 @@ Here is type constructors which are partially constructed with not concrete type
lst = list/1.
functorArg = type/1.
-Here is mix of dependance of concrete types and partially constructed:
+Here is mix of dependence of concrete types and partially constructed:
mixed(T,A) = product(A,any,sum(T,list(T)),product/3,fun/2,functor(list/1)).
@@ -77,7 +77,7 @@ Kinds Notion
------------
Type constructors 'cat', 'fun', 'sum' and 'product' belongs to type 'type' which
-is also typeable by number of arguments and signature of type construdctor:
+is also typeable by number of arguments and signature of type constructor:
Typed Erlang System Fω
------------ ---------
@@ -126,7 +126,7 @@ if capital -- variable.
a = tree(integer()).
B = {1}.
-Exeption is functions which are treated as fun types with binded body values:
+Exception is functions which are treated as fun types with binded body values:
b = tree(integer()) -> {1}.
join = fun(A,B) -> lists:join(A,B) end.
@@ -134,7 +134,7 @@ Exeption is functions which are treated as fun types with binded body values:
Modules
-------
-Modules are paramerized by type constructors, which form local programs.
+Modules are parametrized by type constructors, which form local programs.
tree(A) = sum(product(A),product(tree(A),tree(A))) = {A} | {tree(A),tree(A)}.
Functor = cat(Type::type/1) -> fmap = fun(fun(A,B),Type(A),Type(B)). end.
Hi, this is a very nice project. Since pure is based on the Calculus of Constructions, there are two worries one could have:
Have you thought about these things, or are the irrelevant?
-error({input,X}) -> om:print("Invalid input type: ~p~n",[X]);
-error({output,X}) -> om:print("Invalid output type: ~p~n",[X]);
-error({untyped,X}) -> om:print("No type for: ~p~n",[X]);
-error({mismatch,{X,Y}}) -> om:print("Invalid Application~nExpected type: ~p~nArgument type: ~p~n",[X,Y]);
-error({unbound,U}) -> om:print("Unbound variable ~p.~n",[U]);
-error({app,A}) -> om:print("Only functions may be applied to values ~p.~n",[A]);
It's a known problem AFAIK
Basically, a function from proofs of P true
and P false
to a proof of forall x : Bool . P x
Line number and character, to help generate useful error messages
Cannot wait for #Morte/recursive at 99 iterations takes normal form
After enabling normalization by default
Prod1/Eq test started to fail
{[erased,typed],"Prod1/Eq"},
as was reported by https://travis-ci.org/groupoid/om/builds/116040415
Impredicative Type-Checker with single universe
Ship as single file shell om
powered by mad
.
Currently it requires rebuilding Om;
https://github.com/groupoid/om/blob/abfb02893228947fe3f5208bd647110471d55d30/src/om.erl#L116
And impredicative checker is required for Boolean dependent eliminator in #25
parsing become very slow for resonable terms
(or parser is not linear in time???)
user@note:~/github/groupoid/om$ time (./om a "#sec2all" , mode "new-posets" > /dev/null)
eheap_alloc: Cannot allocate 529782288 bytes of memory (of type "heap").
real 0m44.392s
user 0m40.764s
sys 0m18.952s
user@note:~/github/groupoid/om$ time (./om print type a "#sec2all" , mode "new-posets" > /dev/null)
real 0m45.879s
user 0m44.152s
sys 0m16.196s
test data: https://github.com/groupoid/om/blob/c970619f039433454a06e31b6e9948873cff110c/priv/new-posets/sec2all
This could also solve the problem with pure _
reserved Erlang wildcards during autorenaming.
Also de Bruijn notation leeds us to normal term equality.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.