Namdak Tonpa (maxim) wrote,
Namdak Tonpa
maxim

Infinity Language

Require    Import Strings.String.

Inductive  Loc: Type := intro: string -> nat -> nat -> Loc.
Definition Ident     := string.
Definition Label     := string.
Definition Binder    := prod Ident Loc.
Definition Branch    := prod Label (prod (list Binder) Type).
Definition NamedRec  := list (prod Binder Type).
Definition NamedSum  := list (prod Binder NamedRec).
Definition Decls     := Type.

Inductive PiCalculus :=
 | Send              | Recv
 | Spawn             | Kill
 | Sequential        | Parallel
 | Stop              | Start
 | Pub               | Sub.

Inductive EffectCalculus :=
 | EGet              | ESet
 | ESend             | ERecv
 | Write             | Read
 | Index             | Search
 | Rand              | Raise
 | Try               | Catch.

Inductive StreamCalculus :=
 | Map               | Fold
 | Scan              | Iota
 | SLoop             | Transpose
 | Rotate            | SSplit
 | Concat            | Zip
 | Reduce            | StreamMap
 | StreamMapPer      | StreamRed
 | StreamSeq         | Partition
 | Reshape           | Shape
 | Rearrange         | Copy
 | For               | While.

Inductive HomotopyCalculus :=
 | Id                | Refl
 | Inh               | Inc
 | Squash            | InhRec
 | TransU            | TransInvU
 | TransURef         | CSingl
 | MapOnPath         | AppOnPath
 | HExt              | EquivEq
 | EquivEqRef        | TransUEquivEq
 | IdP               | MapOnPathD
 | AppOnPathD        | Circle
 | Base              | HLoop
 | CircleRec         | I
 | I0                | I1
 | Line              | IntRec
 | Undef: Loc -> HomotopyCalculus.

Inductive MLTT :=
 | App:    MLTT   -> MLTT -> MLTT
 | Pi:     MLTT   -> MLTT -> MLTT
 | Lam:    Binder -> MLTT -> MLTT
 | Sigma:  MLTT   -> MLTT -> MLTT
 | Pair:   MLTT   -> MLTT -> MLTT
 | Fst:    MLTT   -> MLTT
 | Snd:    MLTT   -> MLTT
 | Where:  MLTT   -> Decls -> MLTT
 | Var:    Ident  -> MLTT
 | U:      MLTT
 | Con:    Label  -> list MLTT   -> MLTT
 | Split:  Loc    -> list Branch -> MLTT
 | Sum:    Binder -> NamedSum    -> MLTT
 | HIT:    HomotopyCalculus -> MLTT
 | PI:     PiCalculus       -> MLTT
 | EFF:    EffectCalculus   -> MLTT
 | STREAM: StreamCalculus   -> MLTT.


Скоро будет обновление Групоид Инфинити, я покажу как я вижу сопряжения Coq или Lean и линковку с рантаймами, которые делают пи калкулус (виртуальной машины с каналами) или стрим процессинг (типа футарка, управление GPU или векторизацией). Все это в фашистком стиле с единой вертикалью власти, которая лендится на MLTT коре, но в отличие от ОМ с сигмой и другими излишествами. Если вам интересно вы всегда можете высказаться на канале Infinity Language: http://gitter.im/groupoid/exe

EXE соответственно будет историческим названием конфигурации MLTT + EFF + PI. Без стримов и гомотопической теории. В Групоиде также найдется место для нетипизированных интерпретаторов в виде языка О. Вова по-прежнему топит за лендинг на Erlang, т.е. Coq-Erlang. Экстракт в Erlang и Rust — этими двумя направлениями занимаются японцы. Базовая библиотека передет в System F секцию (так как для рантайма зависимые типы нужны не особо), которая создана для оптимизирующих компиляторов типа Oczor и HNC. Для Oczor я слышал по-секрету скоро появится LLVM бекенд.

Вообще я вижу Групоид Инфинити как журнал, которых захватывает все продакшин применения всех систем типов и их приложений. Так что я думаю пиздить или приглашать публиковаться на тему: как я создал язык X для продакшина или любые достижения и самые модные (но обязательно минималистичные) подходы в каждом из пяти калкулусов. C HoTT как я понял, пока все основные конструкторы бюлтинами не сделаешь, никакого минимализма не получится, зато так даже лучше видно из чего состоит язык геометрии. HoTT и кубическую теорию будем считать продакшином для математиков.

Скину пока только скриншотик:

Tags: cs, groupoid infinity
Subscribe
  • Post a new comment

    Error

    default userpic

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 0 comments