Presentation 20230802 tllhug yuldsl progress report

YulDSL, Linear Haskell & YOLC: A Progress Report

⚠ This file is automatically generated from this org file using this script.

The exported presentation can be accessed via this githack link.

REVISIONS:

Date	Notes
2023-08-02	Tallinn HUG First Meetup Talk.

What You Will Hear About

• What is YulDSL and why?
• “Evaluating Linear Functions to Symmetric Monoidal Categories” ☠.
• Linear Haskell overview.
• What is yolc?

YulDSL

A DSL for Solidity/Yul

• 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.
• YulDSL is a DSL for Yul.

YulDSL as a Categorical Language

Definition of Category

-- 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

Haskell Version of YulDSL (An eDSL, “e” as in Embedded)

-- (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) ()

YulDSL Can Be Implemented in Other Language

• 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

1. Promote Haskell as an advanced alternative to Solidity for building on EVM.
2. Making a case that we should build fewer new languages when some advanced language, such as Haskell, 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 diagram, notably with these “combinators”

An Example SMC Wire Diagram

• This is also called “point-free style.”
• However, this categorical language is difficult for (normal) human brains.

Same Example But With Variables

• 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, in order to understand or construct programs “more naturally.”

Linear Functions to the Rescue

Correspondence Between Linear Functions & SMC

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].

“Frontend for human; mathematics as backend”

• Linear functions are the “frontend language” human can naturally program with.
• SMC is the “backend language” that is compositional; and compositionality is good for:
  • program reusability,
  • compositionally correct methodology (Conal Elliot) for program correctness,
  • etc.

Linear Haskell

-XLinearTypes

A function f is linear if: when its result is consumed exactly once, then its argument is consumed exactly once.

• linearity over the arrow: a %1 ->
• Linear 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

-- | 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

An Demo: In-place QuickSort

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:

   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
       

3. Define additional linear combinators for your domain.
4. Profit.

A Short Example

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)

ERC20 Transfer Function

-- | 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

Command Line

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).

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.
• Arrow and its proc sugar notation also offer a way of wiring computational graphs.
• 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 yul-dsl-monorepo by searching “yuldsl progress”.