The FµN language: From Definition to Execution

Chocolatine

C C++ OCaml Lisp Scheme Haskell Prolog Perl Java Javascript Scala PHP Python Objective-C Swift Rust Kotlin Idris Coq ... FµN

Why designing a language?

• New memory management e.g. Rust
• Explore expressivness e.g. OCaml, Haskell
• Combine paradigms e.g. Scala, λProlog
• Bring property like immutability e.g. Purescript
• Program and Proof e.g. Coq, Idris, Agda
• Or simply because "Yes we can!"

Language Proposition

A functional programming language with primitive data and a naive Javascript interoperability

Abstraction and Application

    def identity = { a -> a }

    def compose  = { f g x -> f $ g x }

    def pipe     = let swap = { a b c -> a c b }
                   in swap compose

    def _        = pipe identity identity
            

Primitive data and Javascript interoperability

    def response = 42

    def hello    = "Hello"

    def pi       = native "pi" (* pi is a JS function *)
            

Example

    def leq?  = { l r t f → native "leq"   } // l <= r ? t : f
    def mult  = { l r     → native "mult"  }
    def minus = { l r     → native "minus" }

    def cond  = { c t f → c t f () }

    def fact  = { a →
       cond (leq? a 1)
            { _ → 1 }
            { _ → mult a (fact (minus a 1)) }
    }

    def _ = fact 12
            

Example :: Simplification

    def leq?  = { l r t f → native "leq"   } // l <= r ? t : f
    def mult  = { l r     → native "mult"  }
    def minus = { l r     → native "minus" }

    def cond  = { c t f → c t f () }

    def fact  = { a →
       cond (leq? a 1)
            { 1 }
            { mult a $ fact $ minus a 1 }
    }

    def _ = fact 12
            

Example :: DSL using CPS

    def yield = { v c → c v         }
    def then  = { v c → yield $ c v }
    def do    = { c   → then () c   }

    def _ = do    { plus 20 4 }
            then  { minus _ 1 }
            then  { minus _ 2 }
            yield $ mult 2
            

Ocaml :: DSL using CPS

    # let yield a c = c a ;;
    val yield : 'a → ('a → 'b) → 'b = <fun>

    # let _then v c = yield @@ c v ;;
    val _then : 'a → ('a → 'b) → ('b → 'c) → 'c = <fun>

    # let _do c = _then () c ;;
    val _do : (unit → 'a) → ('a → 'b) → 'b = <fun>

    # _do (fun () → "3")     (* (string → '_a) → '_a *)
      _then int_of_string    (* (int    → '_b) → '_b *)
      _then (( * ) 4  )      (* (int    → '_c) → '_c *)
      yield (( + ) 30 );;    (* int                  *)
    - : int = 42
            

syntax highlights

EBNF Grammar

    Id  ::= [a-zA-Z_][a-zA-Z0-9_$?]*
    exp ::= Id                      -- Identifier
          | Number                  -- Float literal e.g. -1.3e2
          | String                  -- String literal e.g. "o_O"
          | native String           -- Native binding
          | ()                      -- Unit
          | ( exp+ )                -- Block of application
          | $ exp+                  -- Infix application
          | { (Id+ →)? exp+ }       -- Abstraction à la Kotlin
          | let Id = exp+ in exp+   -- Binding
    def ::= def Id = exp+
    s0  ::= def* 

Analyze

Parsing

Parser combinator

• LL grammars i.e. no left recursion
• Capability to backtrack on-demand
• Based on composition i.e. Monadic
• Test Driven Development compliant

Abstract syntax

    type Ast =
    | ident       of String
    | constant    of Number | String
    | native      of String
    | application of Ast * Ast
    | abstraction of String * Ast
            

From concrete syntax to abstract syntax

 type Native = Number ∪ String

 P⟨_⟩ :: Sequence char → Ast | Error

 P⟨i⟩              = Ast.ident(i)               if i ∈ Id
 P⟨n⟩              = Ast.constant(n)            if n ∈ Native
 P⟨native s⟩       = Ast.native(s)              if s ∈ String
 P⟨()⟩             = Ast.constant(unit)
 P⟨( a )⟩          = P⟨a⟩
 P⟨$ a⟩            = P⟨a⟩
 P⟨{ a -> b }⟩     = Ast.abstraction(a, P⟨b⟩))  if a ∈ Id
 P⟨let a = c in b⟩ = P⟨{ a -> b } c⟩            if a ∈ Id
 P⟨a b⟩            = Ast.application(P⟨a⟩,P⟨b⟩)
      

Transform

De Bruijn index

λ-terms representation without
naming the bind variables

                    λf.((λx.x) (λy.y) (λz.(f z)))
                            ↓      ↓       ↓ ↓
                     λ.( (λ.0)  (λ.0)  (λ.(1 0)))
            

Invariant with respect to α-conversion and direct access in an environment

Abstract syntax

    type AstDB =
    | ident       of String
    | constant    of Number | String
    | native      of String
    | application of Ast * Ast
    | abstraction of Ast              (* No variable binding *)
    | variable    of Number           (* Direct access       *)
            

Determine De Bruijn indexes

 A⟨_⟩ :: Ast → List String → AstDB

 A⟨Ast.constant(c)⟩e       = AstDB.constant(c)
 A⟨Ast.native(c)⟩e         = AstDB.native(c)
 A⟨Ast.application(a,b)⟩e  = AstDB.application(A⟨a⟩e, A⟨b⟩e)
 A⟨Ast.abstraction(a,b)⟩e  = AstDB.abstraction(A⟨b⟩a::e)
 A⟨Ast.ident(n)⟩e          = AstDB.ident(n)    if ∀ i   / e[i]≠n
 A⟨Ast.ident(n)⟩e          = AstDB.variable(i) if ∃ i   / e[i]=n
                                                  ∀ j<i / e[j]≠n
      

Interpret

Operational semantic

 type ResultI = Number | String | (AstDB,Env)
  and Env     = List ResultI

 I⟨_⟩ :: AstDB → Env → ResultI | Error

 I⟨AstDB.constant(c)⟩e       = c
 I⟨AstDB.variable(i)⟩e       = e[i]
 I⟨AstDB.abstraction(b)⟩e    = (b,e)
 I⟨AstDB.application(a,b)⟩e  = I⟨c⟩d::e' when I⟨b⟩e =* d
                                          and I⟨a⟩e =* (c,e')
            

Compile

AstDB ⟹ Objcode

Abstract machine

• P. J. Landin's SECD machine
• L. Cardelli's FAM machine
• Curien's CAM machine

Compilation instructions

    type Objcode =
    | ident    of String
    | constant of Number | String
    | native   of String
    | access   of Number
    | closure  of List Objcode
    | apply
    | returns
            

Compilation process

 C⟨_⟩:: AstDB → List Objcode

 C⟨AstDB.ident(n)⟩         = [Objcode.ident(n)⟩
 C⟨AstDB.constant(c)⟩      = [Objcode.constant(c)⟩
 C⟨AstDB.native(c)⟩        = [Objcode.native(c)⟩

 C⟨AstDB.variable(i)⟩      = [Objcode.access(i)⟩
 C⟨AstDB.application(a,b)⟩ = C⟨a⟩ @ C⟨b⟩ @ [Objcode.apply]
 C⟨AstDB.abstraction(b)⟩   = [Objcode.closure(
                                 C⟨b⟩ @ [Objcode.returns]
                             )]
      

Execute

Execution process :: Core

 type ResultE = Number | String | (Objcode,Env)
  and Env     = List ResultE
  and Stack   = List (ResultE | Env | Objcode)

 E⟨_⟩ :: Objcode list → Env → Stack → ResultE | Error

 E⟨Objcode.access(i)::c⟩e s          = E⟨c⟩e e[i]::s
 E⟨Objcode.closure(c')::c⟩e s        = E⟨c⟩e (c',e)::s
 E⟨Objcode.apply::c⟩e v::(c',e')::s  = E⟨c'⟩v::e' c::e::s
 E⟨Objcode.returns::_⟩e v::c'::e'::s = E⟨c'⟩e' v::s
 ...
    

Execution process :: Extension

 definition :: String → ResultE
 native     :: String → Env → ResultE

 E⟨Objcode.constant(n)::c⟩e s        = E⟨c⟩e n::s
 E⟨Objcode.ident(n)::c⟩e s           = E⟨c⟩e (definition n)::s
 E⟨Objcode.native(n)::c⟩e s          = E⟨c⟩e (native n e)::s
  

Open problem

Function with multiple arguments?

Short lived closures construction and calls that returns immediately!

The X. Leroy's ZINC abstract machine

"From Krivine’s machine to the Caml implementations" - Xavier Leroy

REPL

Sequence char ⟹ Result_E | Error

P⟨_⟩.map(A⟨_⟩_[]).map(C⟨_⟩).map(E⟨_⟩_{[] []}).join()

FµN in a browser

  <script type="application/mfun">    def compute_then_display = { v →
        do    { changeDom "val" v }
        then  { changeDom "res" $ fact v }
        yield { () }
    }

    def _ = compute_then_display 100  </script>

Going further

• Control flow analysis
• Type checker
• Data representation

The FµN language