Phi

Algebraic pure functional language Phi, implementing PureScript and Hamler syntax and sematics, rewritten in Elixir for Erlang/OTP concurrency model.

module Main where import Prelude import Effect.Console (log) main :: Effect Unit main = do log "Hello, Phi!" log "Strongly-typed • Concurrent • Distributed"

Features

Power & Beauty

Write pure functional code. Compile to highly scalable, fault-tolerant Erlang bytecode.

Full Type Safety

Compile-time type checking and inference. Algebraic data types, pattern matching, type classes.

Effectful Concurrency

Actors, OTP behaviours, supervision trees — all with PureScript syntax.

Announcement

$ mix deps.get
$ mix phi.repl
Phi Interactive REPL
Type :quit to exit, :reset to clear bindings
Library loaded. Ready.
ф> import Control.Process
ф> getSelf
#PID<0.94.0>
ф> import Control.Application
ф> loadedApplications
[
  %{name: :logger, vsn: ~c"1.18.4", desc: ~c"logger"},
  %{name: :mix, vsn: ~c"1.18.4", desc: ~c"mix"},
  %{name: :iex, vsn: ~c"1.18.4", desc: ~c"iex"},
  %{name: :phi, vsn: ~c"0.3.1", desc: ~c"The Phi Programming Language",
  %{name: :ex_unit, vsn: ~c"1.18.4"', desc: ~c"ex_unit"},
  %{name: :stdlib, vsn: ~c"7.0.2", desc: ~C"ERTS CXC 138 10"},
  %{name: :crypto, vsn: ~c"5.6"', desc: ~c "CRYPTO" },
  %{name: :compiler, vsn: ~c"9.0.1", desc: ~C"ERTS CXC 138 10"},
  %{name: :elixir, vsn: ~c"1.18.4", desc: ~c"elixir"},
  %{name: :kernel, vsn: ~C"10.3.2"', desc: ~C"ERTS CXC 138 10"}
]

This meant to be learning excercise on how to implement simple educational HM language codenamed Phi (stands for Philosophy, author of PureScript Phil, and Fibonacci misspelling) for Erlang naturally, but things got out of control eventually. Same excercise could and should be applied for Idris for fibrational Pi and Sigma capabilities for those who blatantly dislike the syntax of glorious Coq. As for Miranda syntax for Erlang dependently typed prover I name Sigma project and for Coq inspired architecture there is already project in Groupoid, Christine.

The Christine syntax could should be compatible with Erlang implementation once it emerges. As for technical hints please take the following heart advise:

• Start with classical HM or MLTT typechecker
• Learn Erlang AST complitation by Henk or Per examples
• Don't use Erlang guards for anything as they slowdown compilation
• Don't use Kahn's Topological sort for anything as we are runtime
• In runtime always choose first Type Class instance
• Pay Attention to Curring in code generation
• Pay Attention to FFI
• Pay Attention to Process modality

Properties

• Functional programming
• Functions, higher-order functions
• Algebraic data type (ADT)
• PureScript syntax and Hamler base library
• Compilation of base library in seconds
• Compile-time type checkig and inference
• Currying and partial application
• Pattern matching, and effective guards
• List comprehension
• Featured Absence of HKT
• Applicative and Monad
• Advanced module system
• Built-in concurrency

Credits

This language was created by non-human impersonated spirits of these guys representing canonical lineage:

• Prolog Team (Alain Colmerauer with Philippe Roussel)
• ML/LCF Team (Robin Milner)
• Miranda Team (David Turner)
• Haskell Team (Simon Peyton Jones)
• Erlang Team (Joe Armstrong)
• PureScript Team (Phil Freeman)
• Elixir Team (José Valim)
• Hamler Team (Feng Lee)
• Groupoid Team (Namdak Tonpa)

Open Source