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

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

• 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

(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”.