BekaValentine

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

BekaValentine

("!- \p. (snd p, fst p) : A*B -> B*A"
  "->I"
  ("p : A*B !- (snd p, fst p) : B*A"
    "*I"
    ("p : A*B !- snd p : B"
      "*E2"
      ("p : A*B !- p : A*B"
        "hyp"))
    ("p : A*B !- fst p : A"
      "*E1"

BekaValentine

Keybase proof

I hereby claim:

• I am psygnisfive on github.
• I am darrylmcadams (https://keybase.io/darrylmcadams) on keybase.
• I have a public key whose fingerprint is 6924 6479 FD35 75E7 D5B1 B3D0 E450 3C56 C463 83C0

To claim this, I am signing this object:

BekaValentine

module STLC where




data Ty : Set where
  Zero One : Ty
  _*_ _=>_ _+_ : Ty → Ty → Ty

data Ctx : Set where

BekaValentine

darryl-mcadamss-macbook-pro:test-project darryl$ stack exec new-template-exe slave localhost 8080 & stack exec new-template-exe slave localhost 8081 & stack exec new-template-exe master localhost 8082
[3] 4928
[4] 4929
new-template-exe: bind: resource busy (Address already in use)
new-template-exe: bind: resource busy (Address already in use)
Slaves: [nid://localhost:8080:0,nid://localhost:8081:0]
[1]   Done                    stack exec new-template-exe slave localhost 8080
[2]   Done                    stack exec new-template-exe slave localhost 8081
[3]-  Exit 1                  stack exec new-template-exe slave localhost 8080
[4]+  Exit 1                  stack exec new-template-exe slave localhost 8081

BekaValentine

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ViewPatterns #-}

import Control.Concurrent (threadDelay)
import Control.Distributed.Process
import Control.Distributed.Process.Closure
import Control.Distributed.Process.Node

BekaValentine

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}



module Serialization where

data Nat = Zero | Suc Nat

BekaValentine

open import Data.Bool
open import Data.List
open import Data.Maybe
open import Data.Nat
open import Data.Product

data Tree (A : Set) : Set where
  leaf : Tree A
  branch : Tree A → A → Tree A → Tree A

BekaValentine

infixr 9 _->>_

data Arity : Set where
  * : Arity
  _->>_ : Arity → Arity → Arity

infixl 3 _,_
data Ctx : Set where
  <> : Ctx
  _,_ : Ctx → Arity → Ctx

BekaValentine

(module Validator
  (import Prelude)
  (export validator)
  (local)
  
  ;; validator :: ByteString -> Comp Unit
  (define validator
    (lam sig
      (bind