groupoid / henk Goto Github PK

View Code? Open in Web Editor NEW

144.0 22.0 20.0 10.91 MB

🧊 Чиста система з всесвітами

Home Page: https://henk.groupoid.space

License: Other

CSS 17.98% Elixir 5.24% Erlang 76.77%

pure pts lambda-cube erlang termination

henk's Introduction

Henk: Pure Type System

Henk languages described first by Erik Meijer and Simon Peyton Jones in 1997. Later on in 2015 a new implementation of the ideas in Haskell appeared, called Morte. It used the Böhm-Berarducci encoding of recursive data types into non-recursive terms. Morte has constants, variables, and kinds, is based only on П, λ and apply constructions, one axiom and four deduction rules. The Henk language resembles Henk design and Morte implementation. This language is indended to be small, concise, easily provable, clean and be able to produce verifiable programs that can be distributed over the networks and compiled at target with safe linkage.

$ mix deps.get
$ iex -S mix

The Henk Syntax is the following:

   <> ::= #option

    I ::= #identifier

    U ::= * < #number >

    O ::= U | I | ( O ) | O O
            | λ ( I : O ) → O
            | ∀ ( I : O ) → O

Henk is an implementation of PTS with an Infinite Number of Universes, the pure lambda calculus with dependent types. It can be compiled (code extraction) to bytecode of Erlang virtual machines BEAM and LING.

Trusted PTS with an Infinite Universes

In repository henk you may find the following parts of core:

Henk ships with different "modes" (spaces of types with own encodings), or "preludes", which you may find in lib directory. They are selectable with om:mode("normal").

normal

henk.groupoid.space/lib/normal/
  ├── Bool
  ├── Cmd
  ├── Eq
  ├── Equ
  ├── Frege
  ├── IO
  ├── IOI
  ├── Lazy
  ├── Leibnitz
  ├── List
  ├── Maybe
  ├── Mon
  ├── Monad
  ├── Monoid
  ├── Morte
  ├── Nat
  ├── Path
  ├── Prod
  ├── Prop
  ├── Sigma
  ├── Simple
  ├── String
  ├── Unit
  └── Vector

This is a minimal practical prelude similar to Morte's base library of Gabriella Gonzalez. It contains common inductive constructions encoded using plain Church (or Böhm-Berarducci if you wish) encoding, and two basic (co)monadic effect systems: IO (free monad, for finite I/O) and IOI (free comonad, for infinitary I/O, long-term processes). The generated code is being sewed with Erlang effects that are passed as parameters to pure functions.

Note: all these folders (modules) are encoded in plain CoC in Henk repository to demonstrate you the basic principles how things work. Later all these should be written in Per languages and translated to Henk automatically (if possible). You may think of Henk as the low-level typed assembler of type theory.

PTS

AUTOMATH, a language for mathematics. [Nicolaas Govert de Bruijn]
Lambda Calculi with Types [Henk Barendregt]
The Calculus of Constructions [Thierry Coquand, Gerard Huet]
Introduction to Generalized Type Systems [Henk Barendregt]
Some remarks about Dependent Type Theory [Thierry Coquand]
Henk: a typed intermediate language [Erik Meijer, Simon Peyton Jones]
Morte: an intermediate language for super-optimizing functional programs [Gabriella Gonzalez]
Henk: Pure Type System for Erlang [Maksym Sokhatskyi]
Система доведення теорем з однiєю аксiомою [Maksym Sokhatskyi]

Credits

Maksym Sokhatskyi 🇺🇦

henk's People

Contributors

Stargazers

Watchers

Forkers

e42s m-2k yurrriq nau nponeccop spivakov randl pyzh erlang-cn mafm zabrane ilya-klyuchnikov forked-from-1kasper 5ht-st0le-this-project azcmann

henk's Issues

Travis support

Normalization is too slow

Cannot wait for #Morte/recursive at 99 iterations takes normal form

Examples of normalization corner cases

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.

Implement Type Eraser

parser must emit an error for unresolved file references

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.

Test checker with predicative encodings

Implement #Bool/induction in impredicative setoid encoding

Basically, a function from proofs of P true and P false to a proof of forall x : Bool . P x

Some questions

Hi, this is a very nice project. Since pure is based on the Calculus of Constructions, there are two worries one could have:

Although you can state the induction principle for an inductive type, you can not prove it. So even though you have dependent types, without induction these are not particularly useful (I think).
There is no way to write an efficient pattern matching function for an inductive type in CoC. For example when defining a natural number datatype, you cannot write a predecessor function that runs in O(1).

Have you thought about these things, or are the irrelevant?

Implement test suite

And document a way to run it.

Make stream parsers modular for Exe development

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.

Add build instructions to README

implement term compression optimization

avoid redundant parenthesis in om:print

Parser Error

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

Annotate the AST with source file position

Line number and character, to help generate useful error messages

implement interaction nets for normalization

Implement new Om type-checker with indexed stars

Finish implementation of Hurkens paradox

List/head is O(N)

reference substitution before parsing is exponencially inefficient // do use cache table

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

 -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]);

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.

Type system switch for (im)predicativity

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

  {[erased,typed],"Prod1/Eq"},

as was reported by https://travis-ci.org/groupoid/om/builds/116040415