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 

  • 1 comment