#+title: YulDSL, Linear Haskell & YOLC: A Progress Report
#+subtitle: Tallinn HUG Meetup #1 (2023-08-02)
#+author: Miao, ZhiCheng (@hellwolf)
#+email: zhicheng.miao@gmail.com

#+startup: overview
#+options: num:nil toc:nil timestamp:nil
#+reveal_init_options: navigationMode: "linear", transitionSpeed: "fast"
#+reveal_theme: night
#+reveal_trans: concave
#+reveal_extra_css: ../css/presentation-dark.css
#+-reveal_title_slide_background: ../images/sf-slide-dark2022-bg1.png
#+-reveal_default_slide_background: ../images/sf-slide-dark2022-bg1.png

#+begin_notes :revisions
|       Date | Notes                          |
| 2023-08-02 | Tallinn HUG First Meetup Talk. |
#+end_notes

* What You Will Hear About
#+attr_reveal: :frag (roll-in)
- What is /YulDSL/ and why?
- "Evaluating Linear Functions to Symmetric Monoidal Categories" ☠.
- Linear Haskell overview.
- What is /yolc/?
* YulDSL
** A DSL for Solidity/Yul
#+attr_reveal: :frag (roll-in)
- /Yul/ is an intermediate language designed to support different backends.
- But for now, Yul is tightly coupled with /Solidity/ as its frontend language and /EVM/ (Ethereum Virtual Machine) as
  its backend.
  - Solidity is the de-facto programming language for EVM.
  - "Web3 projects lose over $2 billion to hacks and exploits in 2022" alone.
- /YulDSL/ is a DSL for /Yul/.

** An Yul Example
  #+begin_src yul
object "Contract1" {
    // This is the constructor code of the contract.
    code {
        function power(base, exponent) -> result {
            switch exponent
            case 0 { result := 1 }
            case 1 { result := base }
            default {
                result := power(mul(base, base), div(exponent, 2))
                switch mod(exponent, 2)
                case 1 { result := mul(base, result) }
            }
        }
    }
}
  #+end_src
** /YulDSL/ as a Categorical Language
*** Definition of /Category/
#+begin_src haskell
-- from 'base' library:
-- | A class for categories. Instances should satisfy the laws
--
-- [Right identity] @f '.' 'id'  =  f@
-- [Left identity]  @'id' '.' f  =  f@
-- [Associativity]  @f '.' (g '.' h)  =  (f '.' g) '.' h@
--
class Category cat where
    -- | the identity morphism
    id :: cat a a

    -- | morphism composition
    (.) :: cat b c -> cat a b -> cat a c

-- from 'linear-smc' library
class Category k where
  type Obj k :: Type -> Constraint {-<-}
  id   :: Obj k a => a `k` a
  (∘)  :: (Obj k a, Obj k b, Obj k c)
       => (b `k` c) -> (a `k` b) -> a `k` c
#+end_src
*** Haskell Version of /YulDSL/ (An eDSL, "e" as in Embedded)
#+begin_src haskell
-- (Only an excerpt)
data YulCat a b where
-- ...
  YulId   :: forall a.       YulO2 a a     => YulCat a a
  YulComp :: forall a b c.   YulO3 a b c   => YulCat c b -> YulCat a c -> YulCat a b
-- ...
  YulApFun :: forall a b. YulO2 a b => Fn a b -> YulCat a b
  YulITE   :: forall a  . YulO1 a   => YulCat (BOOL, (a, a)) a
  YulMap   :: forall a b. YulO2 a b => YulCat a b -> YulCat [a] [b]
  YulFoldl :: forall a b. YulO2 a b => YulCat (b, a) b -> YulCat [a] b
-- ...
  YulNot :: YulCat BOOL BOOL
  YulAnd :: YulCat (BOOL, BOOL) BOOL
  YulOr  :: YulCat (BOOL, BOOL) BOOL
  YulNumAdd :: forall a. YulNum a => YulCat (a, a) a
  YulNumNeg :: forall a. YulNum a => YulCat a a
-- ...
  YulSGet :: forall a. YulVal a => YulCat ADDR a
  YulSPut :: forall a. YulVal a => YulCat (ADDR, a) ()
#+end_src
***  /YulDSL/ Can Be Implemented in Other Languages
- For "made in Rust"™ folks.
- Compatible implementations of the DSL in different languages can be a foundation for an interoperable module system
  for them.
** Motivation Behind /YulDSL/
#+attr_reveal: :frag (roll-in)
1) Promote Haskell as a safe alternative to Solidity for building on EVM. Why Haskell?
   * Leverage its strong type system, tooling and library ecosystem.
   * Interopable with Agda, a language suited for writing smart contracts the correctness-by-construction way.
2) Making a case that we should build fewer new languages when some mature language, such as Haskell, that is well suited
   to provide eDSL to new problem domains.
3) Building smart contracts at /Superfluid/ using /YulDSL/.
* Linear Functions & SMC
** The Paper
Bernardy, Jean-Philippe, and Arnaud Spiwack. "Evaluating linear functions to symmetric monoidal categories."
** Symmetric Monoidal Category & Its Wire Diagrams
*** SMC is a formal language for such wiring diagrams, notably with these "combinators"
[[file:smc-combinators.png]]
*** An Example SMC Wire Diagram
[[file:smc-example.png]]

- This is also called "point-free style."
- However, this type of categorical language is difficult for (normal) human brains.
*** Same Example But With Variables
[[file:smc-example-with-variables.png]]

- The "open semicolon" notation is akin to the "(,)" operator in Haskell.
- The familiar Latin letters are so-called "variables" that allow human brains to "delimit" their thinking pattern which
  helps them to understand or construct programs "more naturally."
** Linear Functions to the Rescue
*** Correspondence Between Linear Functions & SMC
#+begin_quote
Indeed, every linear function can be interpreted in terms of an smc. This is a well known fact, proven for example by
Szabo [1978, Ch. 3] or Benton [1995].
#+end_quote
*** "Frontend for human; mathematics as backend"
#+attr_reveal: :frag (roll-in)
- Linear functions is a "frontend language" human can naturally program with.
- SMC is the "backend language" that is mathematical and compositional. Compositionality is good for:
  - program reusability,
  - /compositionally correct/ methodology (Conal Elliot) for program correctness,
  - etc.
* Linear Haskell
** ~-XLinearTypes~
#+begin_quote
A function f is linear if: when its result is consumed exactly once, then its argument is consumed exactly once.
#+end_quote
- linearity over the arrow: ~a %1 ->~
- Multiplicity-polymorphism: ~forall a b w. a %w -> b~
- Status: experimental and has limitations.
** Relevant Libraries
*** linear-base
- ~Prelude.Linear~ as a linear replacement for ~Prelude~.
- Additional primitives specific for programming linear functions: ~Consumable~, ~Moveable~, ~Unrestricted~, etc.
- Some functions may require ~-XImpredicativeTypes~ additionally.
*** linear-smc
#+begin_src haskell
-- | A port represents an input or an output of type @a@ of a morphism in the SMC.
data P k r a

-- | Encode a morphism in the SMC to linear function from port @a@ to port @b@
encode :: O3 k r a b => (a `k` b) -> P k r a %1 -> P k r b~

-- | Decode a linear function from port @a@ to port @b@ to its morphism in the SMC.
decode :: forall a b k con.
          ( con (), con ~ Obj k, Monoidal k, con a, con b
          , forall α β. (con α, con β) => con (α, β)
          )
       => (forall r. Obj k r => P k r a %1 -> P k r b)
       -> a `k` b
#+end_src
** An Demo:  In-place QuickSort
[[file:linear-haskell-demo.hs][linear-haskell-demo.hs]]

(taken from a Tweag blog post)
* YOLC: A Frontend for YulDSL
** Using Linear Haskell & SMC
*** The linear-smc Playbook
1) Define your DSL as a categorical language.
2) Define SMC instances for your DSL:
   #+begin_src haskell
instance Category YulCat where
  type Obj YulCat = YulObj
  id  = YulId
  (∘) = YulComp

instance Monoidal YulCat where
  (×)     = YulProd
  unitor  = YulCoerce
  unitor' = YulCoerce
  assoc   = YulCoerce
  assoc'  = YulCoerce
  swap    = YulSwap

instance Cartesian YulCat where
  dis = YulDis
  dup = YulDup
   #+end_src
3) Define additional linear combinators for your domain.
4) Profit.
*** A Short Example
#+begin_src haskell
rangeSum :: Fn (UINT256 :> UINT256 :> UINT256) UINT256
rangeSum = defun "rangeSum" \(a :> b :> c) ->
  dup2P a & \(a, a') ->
  dup2P b & \(b, b') ->
  dup2P c & \(c, c') ->
  dup2P (a + b) & \ (d, d') ->
  mkUnit a' & \(a', u) ->
  a' + ifThenElse (d <? c) (apfun rangeSum (d' :> b' :> c')) (yulConst 0 u)
#+end_src

- A non-linear functions sub-language to calculate these pure values may be more handy to write.
- ~ifThenElse~ is suited to be used in conjunction with the ~RebindableSyntax~ extension.
*** ERC20 Transfer Function
#+begin_src haskell
-- | ERC20 transfer function (no negative balance check for simplicity).
erc20_transfer :: Fn (ADDR :> ADDR :> UINT256) BOOL
erc20_transfer = defun "transfer" \(from :> to :> amount) ->
  (copyAp amount
    (\amount -> passAp from erc20_balance_of & \(from, balance) ->
        erc20_balance_storage from <== balance - amount)
    (\amount -> passAp to erc20_balance_of & \(to, balance) ->
        erc20_balance_storage to <== balance + amount)) &
  yulConst true
#+end_src
*** ~yolc~ command line interface
#+begin_example
nix-shell$ yolc -h
yolc, the YulDSL commandline transpiler.

Usage: yolc [options] yol_module_spec...

-m [output_mode] Valid output modes: show, plantuml, yul (default)
-h               Display this help and exit
-v               Output more information about what is going on

yol_module_spec: {package_path:}module_name{[symbol...,]}
  where 1) both package_path and symbol list is optional,
        2) default package_path is current working directory (/home/hellwolf/Projects/my/yul-dsl-monorepo),
        3) and default symbol is 'defsym' (TODO, use object instead).
#+end_example
*** Full Pipeline
#+begin_src plantuml :file yolc-pipeline.png
scale 500 height

artifact "YulDSL in Haskell" as hsyuldsl
artifact "YulDSL in Rust :D" as rsyuldsl
artifact "Visual Block for YulDSL" as vbyuldsl
agent yolc
artifact "Yul code" as yulcode
agent solc
artifact "EVM Bytecode" as evmbin
agent forge
artifact "EVM Network Instance" as evmnetwork
hsyuldsl -down-> yolc : Compile to YulDSL
rsyuldsl -down-> yolc : Compile to YulDSL
vbyuldsl -down-> yolc : Editing YulDSL visually
yolc     -down-> yulcode : Code generation
yulcode  -down-> solc : Pass yul to solc
solc     -down-> evmbin: Compile yul to binary
evmbin   -down-> forge : Pass to foundry
forge    -down-> evmnetwork : Use foundry to deploy the binary
#+end_src

#+RESULTS:
[[file:yolc-pipeline.png]]

** Demo
!NOTE!: the work is still in its early stage.
* Other Approaches
** Since SMC is well suited for visually programming your program formally, so does /YulDSL/, e.g.:
  - block-based programming: https://blockell.netlify.app/
  - https://code.world/blocks
** Arrow and its ~proc~ sugar notation also offer a way of wiring computational graphs:
#+begin_src haskell
ArrowPlus a => (<+>) :: a b c -> a b c -> a b c

expr' = (proc x -> returnA -< x)
        <+> (proc x -> do
                symbol Plus -< ()
                y <- term -< ()
                expr' -< x + y)
        <+> (proc x -> do
                symbol Minus -< ()
                y <- term -< ()
                expr' -< x - y)
#+end_src
** Other Categories
- Traced monoidal category provides an additional notion of feedback over SMC.
- /YulDSL/ has a richer structure than SMC, namely also cartesian closed.
  - Cartesian closed category (CCC) is correspondent to lambda-calculus, hence normal Haskell function can even be
    translated to CCC.
  - There are various compiling to categories projects. The most notable one is from Conal Elliott. But due to the
    production-readiness, it is harder to set it up.
** What's Next for YulDSL & YOLC?
- Feature complete.
- Ship it!
* Thank You
Slides available from the wiki area of the [[https://github.com/hellwolf/yul-dsl-monorepo/wiki][yul-dsl-monorepo]] by searching "yuldsl progress".