Skip to content

Presentation 20230802 tllhug yuldsl progress report

Jump to bottom
Miao, ZhiCheng edited this page Aug 1, 2023 · 10 revisions

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 in brief.
  • 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)

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 Defined in Other Language

  • “It can be done in Rust.”™
  • Compatible implementations of the DSL in different language can be a foundation for an interoperable module system between them.

Motivation Behind YulDSL

  1. Promote Haskell an advanced alternative to Solidity to build 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 “combinators”

A Example SMC Wire Diagram

smc-example.png

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

Same Example But With Variables

  • The “open semicolon” notation is akin to what “(,)” is in Haskell.
  • The familiar Latin letters are so-called “variables” that allow human brain to “delimit” its thinking patterns, in order to understand or construct such program “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: %1 ->
  • Linear polymorphism: forall w. a %w -> b
  • Status: experimental and with 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?

Ship it!

Thank You

Slides available from the wiki area of the yul-dsl-monorepo by searching “yuldsl progress”.

Clone this wiki locally