This the multi-page printable view of this section. Click here to print.

Return to the regular view of this page.

S-expression Syntax

The concrete syntax of the Juvix syntax after turning into a LISP

1: Core S-Expression Syntax

This document is bound to change once a syntax redesign will happen. This will be greatly minimized

For this page we give examples of the syntax rather than a hard bnf unlike what is found in the syntax page

Generation

Top Level

Let

basic

input

  let foo x
    | x == 2 = 3 + 4 + x
    | else   = x + 2

output

  (:defun foo (x)
    (:cond
      ((:infix == x 2) (:infix + 3 (:infix + 4 x)))
      (else            (:infix + x 2))))

Sig

basic

input
```
  sig foo : int -> int -> int
```

output

  (:defsig foo (:infix -> int (:infix -> int int)))

usage

input
```
  sig foo 0 : int -> int -> int
```

output

  (:defsig foo (:usage 0 (:infix -> int (:infix -> int int))))

This form is a bit odd, ideally it'd mimic the Types version like
```
  (:defsig (foo :usage 0) (:infix -> int (:infix -> int int)))
```
- However for now I think it's fine… Though this is a place for improvement for the future

Types

record

input

  type foo x y z =
    { y-axis : y
    , x-axis : x
    , z-axis 1 : z }

output

  (type foo (x y z)
     (:record-d
       (y-axis (:primitve Builtin.Omega) y)
       (x-axis (:primitve Builtin.Omega) x)
       (z-axis 1 z)))

first sum

input

  type foo x y z =
    | Foo {y-axis : y, x-axis : x, z-axis : z}
    | Bar (var1 : x) (var2 : y)
    | Car : hd : x -> cdr : foo y -> foo x y z

output

  (type foo (x y z)
    (Foo (:record-d (y-axis (:primitve Builtin.Omega) y)
                    (x-axis (:primitve Builtin.Omega) x)
                    (z-axis (:primitve Builtin.Omega) z)))
    (Bar (:paren (:infix : var1 x))
         (:paren (:infix : var2 y)))
    (Car (:arrow
          (:infix : hd
                  (:infix -> x
                          (:infix : cdr
                                  (:infix -> (foo y) (foo x y z))))))))

Signature

input

  type foo x y z : typ -> typ -> typ = Foo a b c

output

  (type (foo :type (:infix -> typ (:infix -> typ typ))) (x y z)
     (Foo a b c))

Decalration

basic

input
```
  declare infixl foo 3
```
output
```
  (declare infixl foo 3)
```

Module

basic

input

  mod foo =
    let bar = 3
    type zar = Boo
  end

output

  (:defmodule foo ()
    (:defun bar () 3)
    (type zar () (Boo)))

guards

input

  mod foo x
    | x == 3 =
      let foo = 3
      let bar = 5
    | else =
      let foo = 5
  end

output

  (:defmodule foo (x)
    (:cond ((:infix == x 3)
            (:defun foo () 3)
            (:defun bar () 5))
           (else
            (:defun foo () 5))))

Expression

Let

basic

input
```
  let foo y =
    let fi = 3 in
    fi
```

output

  (:defun foo (y)
    (let fi () 3
      fi))

arguments

input

  let foo y =
    let fi x = 3 + x in
    fi y

output

  (:defun foo (y)
    (let fi (x) (:infix + 3 x)
      (fi y)))

Module

basic

input

  let foo =
    mod Bar =
      let bar = 3
      type zar = Boo
    end in
    Bar.bar

output

  (:defun foo ()
    (:let-mod Bar ()
       ((:defun bar () 3)
        (type zar () (Boo)))
      Bar.bar))

Tuples

basic

input
```
  let foo = (1,2,3)
```
output
```
  (:defun foo () (:tuple 1 2 3))
```

Lists

basic

input
```
  let foo = [1,2,3,4]
```
output
```
  (:defun foo () (:list 1 2 3 4))
```

Records

basic

input
```
  let foo = {a, b = 2}
```
output
```
  (:defun foo () (:record (a) (b 2)))
```

Do

basic

input

  let foo xs =
    a <- xs;
    more-comp;
    pure a

output

  (:defun foo (xs)
    (:do (%<- a xs)
         more-comp
         (pure a)))

Lambda

basic

input
```
  let foo y =
    \x -> x + y
```

output

  (:defun foo (y)
    (:lambda (x) (:infix + x y)))

Open

basic

input

  let foo y =
    open Prelude in
    x + y

output

  (:defun foo (y)
    (:open-in Prelude
       (:infix + x y)))

Parens

basic

input
```
  let foo y = (y + 3) * 9
```

output

  (:defun foo (y)
    (:infix * (:paren (:infix + y 3)) 9))

Block

basic

input
```
  let foo y = 3 * begin y + y end
```

output

  (:defun foo (y)
    (:infix * 3 (:progn (:infix + y y))))

Primitive

basic

input
```
  let add = %Michelson.add
```

output

  (:defun add ()
    (:primitive Michelson.add))

Declaration

basic

input
```
  let foo = declare infixl (+) 3 in 3
```

output

  (:defun foo ()
    (:declaim (infixl + 3) 3))

Cond

basic

input

  let add x =
    if | x == 3 = 1
       | x == 4 = 5
       | else   = 0

output

  (:defun add (x)
    (:cond ((:infix == x 3) 1)
           ((:infix == x 4) 5)
           (else            0)))

Case

basic

input

  let foo =
     case x of
     | (A (B {a, b})) -> a + b
     | A (B c) (C d)  -> c + d

output

  (:defun foo ()
     (case x
        ((A (B (:record (a) (b)))) (:infix + a b))
        ((A (B c) (C d))           (:infix + c d))))

Notes

Design Principles

Overall the goal of the S-expression incantation is twofold ¹.

An unambiguous syntax that is faithful to the original ML syntax
- This is a necessity to have limited strife between the ML syntax. and the work we need to do on the generic IR-syntax layer.
- Unambiguous in this case implies bijection, as we have to convert between the two forms.
A fully realized syntax that is readable and looks as if it were a standalone language.
- This is needed so inspection of the output is obvious. Further this will empower ease of reasoning over the syntax without too many surprises.

On Verbosity

Overall a few forms in this representation are quite verbose and thus harder to read than they should be, see


  (:arrow
   (:infix : hd
           (:infix -> x
                   (:infix : cdr
                           (:infix -> (foo y) (foo x y z))))))

  ;; should be
  [ hd : x -> cdr : (foo y) -> (foo x y z) ]

  (:record
   y-axis y
   x-axis x
   z-axis z)

  ;; should be
  {y-axis y
   x-axis x
   z-axis z}

This is due to lacking reader macros at this level. Overall this can be largely improved in the future for better inspection (we thus will offer another level of inspection that can do away with the infix view!)

On Forms

The syntax is heavily inspired from Common Lisp (CL). There are of course a plethora of changes, however some key concepts have survived through this transition.

Namely for adding extra property based information in declarations we got for an alist concept

  (type (foo :type (:infix -> typ (:infix -> typ typ))) (x y z)
     (Foo a b c))

which is taken directly from CL's defstruct construct.

Even naming conventions like defun are lifted directly from Common Lisp.

With that said, many forms (namely the lets) lack an extra set of parenthesis when in comparison to CL and the Schemer language.

  (let fi (x) (:infix + 3 x)
      (fi y))

  (let fi () 3
      fi)

This is due to us fully abusing the fact that we must represent non let blocks currently along with having a single expression each name is bound to.

Inconsistencies

There are likely inconsistencies between some of the forms. These should be removed as soon as possible. I have tried my best on this front, but likely some forms are inconsistent.

Known

Signatures

Currently we have a minor point of alists on the name itself to describe extra properties

  (type (foo :type (:infix -> typ (:infix -> typ typ))) (x y z)
     (Foo a b c))

This is great and we'll be adding it to Modules, however we currently do an odd transformation in regards to signatures

  (:defsig foo (:usage 0 (:infix -> int (:infix -> int int))))
  ;; should be
  (:defsig (foo :usage 0) (:infix -> int (:infix -> int int)))

This likely should be changed

Footnotes

The Whimsical spell like nature of sexpressions are heavily derived from SICP and the general imagery of other literature such as the dragon book.

1 - Core S-Expression Syntax

The concrete syntax of Juvix once we Hit Core, namely the Named version (HR)

Generation

Term

Star

Haskell ADT

  = -- | (sort i) i th ordering of (closed) universe.
    Star Universe

ML Syntax

  -- Universe 0
  ×₀
  -- Universe 1
  ×₁
  -- Universe n
  ×ₙ

S-expression Syntax

  ;; universe 0
  (:star 0)
  ;; universe 1
  (:star 1)
  ;; universe n
  (:star n)

Prim type

Haskell ADT

  | -- | PrimTy primitive type
    PrimTy primTy

ML Syntax
```
  primTy Michelson.Int
```
S-expression Syntax
```
  (:prim-ty Michelson.add)
```

Prim

Haskell ADT

  | -- | primitive constant
    Prim primVal

ML Syntax
```
  prim Michelson.Add
```
S-expression Syntax
```
  (:prim Michelson.add)
```

Π / Pi

Haskell ADT

  | -- | formation rule of the dependent function type PI.
    -- the Usage(π) tracks how many times x is used.
    Pi Usage NameSymbol.T (Term primTy primVal) (Term primTy primVal)

ML Syntax

  (Π (0 | typ : ×₀) (Π (1 | _ : typ) typ))

S-expression Syntax

  (:pi (typ 0 (:star 0)) (:pi (_ 1 typ) typ))

Lam

Haskell ADT

  | -- | LAM Introduction rule of PI.
    -- The abstracted variables usage is tracked with the Usage(π).
    Lam NameSymbol.T (Term primTy primVal)

ML Syntax

  -- Note we don't have (λ x : unit -> x) : unit -> unit, as that requires
  -- the type to be given in the Haskell ADT, and is thus handled in Π
  λ x ⟶ ∅

S-expression Syntax
```
  (:named-lambda x :unit)
```

Sig

Haskell ADT

  | -- | Dependent pair (Σ) type, with each half having its own usage
    Sig Usage NameSymbol.T (Term primTy primVal) (Term primTy primVal)

ML Syntax

  Π (ω | x : A) ⟶
    Σ (ω | y : B) ⟶
     C x y

S-expression Syntax

  (:pi (x ω A)
     (:sigma (y ω b)
        (C x y)))

Pair

Haskell ADT

  | -- | Pair value
    Pair (Term primTy primVal) (Term primTy primVal)

ML Syntax
```
  ‹f x y, g x y›
```
S-expression Syntax
```
  (:pair (f x y) (g x y))
```

Let

Haskell ADT

  | -- | Let binder.
    -- the local definition is bound to de Bruijn index 0.
    Let Usage NameSymbol.T (Elim primTy primVal) (Term primTy primVal)

ML Syntax
```
  let 2 | a = f x y in
    <a,a>
```

S-expression Syntax

  (:named-let (a 2 (f x y))
    (:pair a a))

Unit type

Note
Should this be treated specially?
Haskell ADT
```
  | -- | Unit type.
    UnitTy
```
ML Syntax
```
  Unit
```
S-expression Syntax
```
  :unit-type
```

Unit

Note
Should this be treated specially?
Haskell ADT
```
  | -- | Unit Value
    Unit
```
ML Syntax
```
  ∅
```
S-expression Syntax
```
  :unit
```

Elim

Should we even have Elims with this strategy, we know by exclusion, an explicit tome for it seems needless? Depends how the code turns out.

Record

Haskell ADT

  | -- | Constructor for a record type.
    Record [(Symbol, Term primTy primVal)]

ML Syntax

  {name₁ = term₁, name₂ = term₂, …, nameₙ = termₙ}

S-expression Syntax

  (:record name₁ term₁ name₂ term₂ … nameₙ termₙ)

RecordTy

Haskell ADT

  | -- | Record type. (It's a list not a map because the dependency order
    -- needs to be preserved.)
    RecordTy [(Symbol, Usage, Term primTy primVal)]

ML Syntax

  {name₁ usage₁ : term₁, name₂ usage₂ : term₂, …, nameₙ usageₙ : termₙ}

S-expression Syntax

  (:record-ty
    (name₁ usage₁ term₁)
    (name₂ usage₂ term₂)
    ...
    (nameₙ usageₙ termₙ))

Elim

Var

Haskell ADT

  = -- | Named Variables
    Var NameSymbol.T

ML Syntax
```
  λ x ⟶ x
```
S-expression Syntax
```
  (:named-lambda x x)
```
- We treat vars as simple any atom in the list that isn't a special form.

App

Haskell ADT

  | -- | elimination rule of PI (APP).
    App (Elim primTy primVal) (Term primTy primVal)

ML Syntax
```
  f a b
```
S-expression Syntax
```
  (f a b)
```
- We simply represent application as the car of the list if it's not a special form

Ann

Haskell ADT

  | -- | Annotation with usage.
    Ann Usage (Term primTy primVal) (Term primTy primVal) Universe

ML Syntax
```
  (ω | f x y : C x y : * 0)
```

S-expression Syntax

  (: (f x y) (:usage ω :universe 0)
     (C x y))

  ;; Should we adopt it without names?
  (: (f x y) (ω 0)
     (C x y))

Here we have a choice, I′m not sure which one I prefer, the first is more explicit, but may be a bit too verbose

Lookup

Haskell ADT

  | -- | Project an element from a record type.
    Lookup (Elim primTy primVal) Symbol

ML Syntax
```
  name.elim
```
S-expression Syntax
```
  (:lookup elim name)
```

Value

Instead of giving each variant a section, we will instead note that Values relate to Terms, except instead of an Elim they have a Neutral.

Thus, it's an extension of Term.

Neutral

Neutral is the same as Value, except we remove annotations from the possibilities

Pattern

Constructor

Haskell ADT

  = PCon GlobalName [Pattern primTy primVal]

ML Syntax
```
  (Cons a as)
```

S-expression Syntax

  ;; No other form has an unattended name with arguments, so this is
  ;; safe
  (Cons a as)

Pair

Haskell ADT

  | PPair (Pattern primTy primVal) (Pattern primTy primVal)

ML Syntax

  -- We have syntax for multi pairs
  ‹x, y, z›
  -- This is just an alias for
  ‹x, ‹y, z››

S-expression Syntax

  (:pair x y z)
  ;; This is just an alias for
  (:pair x (:pair y z))

Unit

Note
Should this be treated specially?
Haskell ADT
```
  | PUnit
```
ML Syntax
```
  ∅
```
S-expression Syntax
```
  :unit
```

Var

Haskell ADT
```
  | PVar PatternVar
```
ML Syntax
```
  (Constructor a b c)

  a

  z
```
S-expression Syntax
```
  (Constructor a b c)

  a

  z
```

Dot

Haskell ADT

  -- Deduction by the unifier, that the term should already be
  -- known
  | PDot (Term primTy primVal)

ML Syntax

  -- Taken From
  -- data Double (n : ℕ) : ℕ → Set where
  --   double : Double n (n + n)

  -- foo : ∀ m n → Double m n → {!!}
  -- foo m .(m + m) double = {!!}

  .(m + m)

S-expression Syntax
```
  (:dot (+ m m))
```

Primitive

Haskell ADT
```
  | PPrim primVal
```
ML Syntax
```
  (Prim +)
```
S-expression Syntax
```
  (:prim +)
```

Raw Globals

This is the target that the context type should hold. However we have to note a few facts about how things are stored.
We don't really have ML syntax counterparts for these, so instead we will give the raw structure as the syntax.

FunClause

In this the full type has many overlapping elements, thus we should just steal the RawFunClause field

Haskell ADT

  data RawFunction' ext primTy primVal = RawFunction
    { rawFunName :: GlobalName,
      rawFunUsage :: GlobalUsage,
      rawFunType :: Term' ext primTy primVal,
      -- The value we want
      rawFunClauses :: NonEmpty (RawFunClause' ext primTy primVal)
    }
    deriving (Generic)

  -- The Type that we will emulate
  data RawFunClause' ext primTy primVal = RawFunClause
    { rawClauseTel :: RawTelescope ext primTy primVal,
      rawClausePats :: [Pattern' ext primTy primVal], --TODO [SplitPattern]
      rawClauseBody :: Term' ext primTy primVal,
      rawClauseCatchall :: Bool
    }
    deriving (Generic)

Haskell Context ADT

  data Def term ty = D
      -- This mimics rawFunUsage
    { defUsage :: Maybe Usage.T,
      -- This mimics rawFunType
      defMTy :: Maybe ty,
      -- This field will mimic rawFunClause'
      defTerm :: term,
      defPrecedence :: Precedence
    }
    deriving (Show, Read, Generic, Eq, Data)

Raw Fun Clause Example

  RawFunClause
    { rawClauseTel = []
    , rawClausePats =
        [ PVar "x" ]
    , rawClauseBody = Elim'
                      ( Var "x" )
    , rawClauseCatchall = False } :| []

Currently I can't get a better example sadly.

S-expression Syntax

  (:raw-fun-clause () (x)
    x
    :false)