Skip to content

Instantly share code, notes, and snippets.

@m1dnight

m1dnight/Main.hs

Created June 29, 2016 18:27
Show Gist options
  • Save m1dnight/8f3b8c34a1f5a718bd3ff854c41ebe59 to your computer and use it in GitHub Desktop.
Save m1dnight/8f3b8c34a1f5a718bd3ff854c41ebe59 to your computer and use it in GitHub Desktop.
Download ZIP
Session Typed Lambda Calculus (Vasconcelos 2006)
Raw
Main.hs
module Main where
import Control.Arrow
import Debug.Trace
import Control.Monad.State
import Data.List hiding (union)
import Data.Maybe
import Syntax
import Text.Printf
-- ____ _ _____ _
-- / ___| ___ ___ ___(_) ___ _ __ |_ _| _ _ __ ___ __| |
-- \___ \ / _ \/ __/ __| |/ _ \| '_ \ | || | | | '_ \ / _ \/ _` |
-- ___) | __/\__ \__ \ | (_) | | | | | || |_| | |_) | __/ (_| |
-- |____/ \___||___/___/_|\___/|_| |_| |_| \__, | .__/ \___|\__,_|
-- |___/|_|
-- | | __ _ _ __ ___ | |__ __| | __ _ / ___|__ _| | ___ _ _| |_ _ ___
-- | | / _` | '_ ` _ \| '_ \ / _` |/ _` | | | / _` | |/ __| | | | | | | / __|
-- | |__| (_| | | | | | | |_) | (_| | (_| | | |__| (_| | | (__| |_| | | |_| \__ \
-- |_____\__,_|_| |_| |_|_.__/ \__,_|\__,_| \____\__,_|_|\___|\__,_|_|\__,_|___/
--
-- Based on the work by Vasconcelos et al.
-- Vasconcelos, V. T., Gay, S. J., & Ravara, A. (2006). Type checking
-- a multithreaded functional language with session types. Theoretical
-- Computer Science. http://doi.org/10.1016/j.tcs.2006.06.028
-----------
-- Notes --
-----------
-- 1) One thing I did not notice at first was that all the expression
-- are in A-normal form:
-- https://en.wikipedia.org/wiki/A-normal_form. This makes the
-- typechecker a lot easier because you can make assumptions about
-- the actual result of typing an expression, namely that they are
-- all values.
--------------------------------------------------------------------------------
--- HELPERS --------------------------------------------------------------------
--------------------------------------------------------------------------------
-- Extend environment.
extend env v t = case lookup v env of
Just t -> error $ printf "Shadowing binding of variable: %s to %s, in %s" (show v) (show t) (show env)
Nothing -> (v,t):env
-- Union two environments (pointwise extend).
union = foldr (\e acc -> (uncurry $ extend acc) e)
-- Extract a binding from the environment.
-- Assumes that there are only unique keys in the environment!
extract key env = case partition (\(k,v) -> k == key) env of
([(_,v)], rest) -> (v, rest)
_ -> error "key not found"
-- Pointwise extraction
extractset env env' = foldr (\(k,v) acc -> snd $ extract k acc) env' env
-- Generate fresh variable name.
--fresh = AId "freshid"
fresh = do i <- get
put (1 + i)
return $ AId (show i)
-- Check if a label exists in a given in/external choice.
validLabel cs lbl = isJust $ lookup lbl cs
-- All elements of the list equal to eachother?
allsame [] = True
allsame xs = all (head xs ==) (tail xs)
-- Dual of a session type.
dual (SReceiveD d s) = SSendD d (dual s)
dual (SSendD d s) = SReceiveD d (dual s)
dual (SReceiveS s s') = SSendS s' (dual s)
dual (SSendS s s') = SSendS s' (dual s)
dual (SExternal lss) = SInternal $ map (second dual) lss
dual (SInternal lss) = SExternal $ map (second dual) lss
dual SEnd = SEnd
--------------------------------------------------------------------------------
--- TYPECHECKER ----------------------------------------------------------------
--------------------------------------------------------------------------------
-- The state is just an integer.
type St = Integer
------------
-- Values --
------------
typeVal :: [(String, S)] -> [(String, Typ)] -> V -> State St ([(String, S)], Typ, [(String, S)])
-- C-Const
-- Γ ; unit ↦ Unit
typeVal sigma gamma VUnit = return (sigma, TD DUnit, [])
typeVal sigma gamma (VNum i) = return (sigma, TD DNum, [])
-- C-Chan
-- Γ ; γᵖ ↦ Chan γᵖ
typeVal sigma gamma (VAlpha chanid) = return (sigma, Chan chanid, [])
-- C-Var
-- Γ,x:T ; x ↦ T
typeVal sigma gamma (VVar var) = let mvarT = lookup var gamma
in
return (sigma, fromMaybe (error $ printf "Variable %s unbound" var) mvarT, [])
-- C-Abs
-- Γ,x:T ; Σ; e ↦ Σ₁;U;Σ₂
-- -----------------------------------
-- Γ ; λ(Σ;x:T).e ↦ (Σ;T → U;Σ₁,Σ₂)
typeVal sigma gamma (VLambda σ x t e) = do let gamma' = (x,t):gamma
(σ1, u, σ2) <- typeExp sigma gamma' e
return (sigma, TD $ DArrow σ t u (σ1 `union` σ2), [])
-- C-Rec
-- Γ,x:T ; v ↦ T T = (Σ;U → U';Σ')
-- ----------------------------------
-- Γ ; rec(x:T).v ↦ T
typeVal sigma gamma (VRec x t v) = let gamma' = extend gamma x t
in
do (_, typ, _) <- typeVal sigma gamma' v
return (sigma, typ, [])
-----------------
-- Expressions --
-----------------
typeExp :: [(String, S)] -> [(String, Typ)] -> E -> State St ([(String, S)], Typ, [(String, S)])
-- C-ReceiveD
-- Γ ; v ↦ Chan α
-- --------------------------------------
-- Γ ; Σ,α:?D.S ; receive v ↦ Σ ; D ; α:S
-- C-ReceiveS
-- Γ ; v ↦ Chan α c fresh
-- -------------------------------------------------
-- Γ; Σ,α:?S'.S ; receive v ↦ Σ ; Chan c ; c:S', α;S
typeExp sigma gamma (EReceive v) = do (_,Chan α,_) <- typeVal sigma gamma v
let (st, σ) = extract (cid α) sigma
case st of
(SReceiveD d s) -> return (σ, TD d, [(cid α, s)])
(SReceiveS s' s) -> do c <- fresh
return (σ, Chan c, [(cid c, s'), (cid α, s)])
-- C-SendD
-- Γ ; v' ↦ Chan α Γ ; v ↦ D
-------------------------------------------------------
-- Γ ; Σ, α:!D.S ; send v on v' ↦ Σ ; Unit ; α:S
-- C-SendS
-- Γ ; v' ↦ Chan α Γ ; v ↦ Chan β
-------------------------------------------------------
-- Γ ; Σ, α:!S'.S, β:S' ; send v on v' ↦ Σ ; Unit ; α:S
typeExp sigma gamma (ESend v v') = do (_,Chan α,_) <- typeVal sigma gamma v'
(_,vT,_) <- typeVal sigma gamma v
let (stα, σ) = extract (cid α) sigma
case stα of
(SSendD d s) -> if TD d /= vT
then error "Types for session do not match sent value."
else return (σ, TD DUnit, [(cid α, s)])
(SSendS s' s) -> let (Chan β) = vT
(stβ, σ') = extract (cid β) σ
in
if s' /= stβ
then error "Session types do not match for sending channel"
else return (σ', TD DUnit, [(cid α, s)])
-- C-Select
-- Γ ; v ↦ Chan α j ∈ I
-----------------------------------------------------------
-- Γ ; Σ, α:⊕⟨lᵢ : Sᵢ⟩ ; select lⱼ on v ↦ Σ ; Unit ; α : Sⱼ
typeExp sigma gamma (ESelect l v) = do (_,Chan α,_) <- typeVal sigma gamma v
let (stα, σ) = extract (cid α) sigma
case stα of
(SExternal cs) -> if validLabel cs l
then let si = fromMaybe (error "Oops?") $ lookup l cs
in
return (σ, TD DUnit, [(cid α, si)])
else error "Invalid label selected."
-- C-Case
-- Γ ; v ↦ Chan α ∀ j ∈ I.(Γ ; Σ,α:Sⱼ ; eⱼ ↦ Σ₁ ; T ; Σ₂)
------------------------------------------------------------
-- Γ ; Σ,α:&⟨lᵢ : Sᵢ⟩ ; case v of {lᵢ ⇒ eᵢ} ↦ Σ₁ ; T ; Σ₂
typeExp sigma gamma (ECase v les) = do (_,Chan α,_) <- typeVal sigma gamma v
let (stα, σ) = extract (cid α) sigma
case stα of
(SInternal cs) -> do casetypes <- mapM typeCase les
if allsame casetypes
then return $ head casetypes
else error "Not all cases have the same type"
where typeCase (lj,ej) = if validLabel cs lj
then let sj = fromMaybe (error "") $ lookup lj cs
in
typeExp sigma gamma ej
else error "Invalid label in case"
-- C-Close
-- Γ ; v ↦ Chan α
---------------------------------------
-- Γ ; Σ,α:End ; close v ↦ Σ ; Unit ; ∅
typeExp sigma gamma (EClose v) = do (_,Chan α,_) <- typeVal sigma gamma v
let (stα, σ) = extract (cid α) sigma
case stα of
SEnd -> return (σ, TD DUnit, [])
-- C-Accept
-- Γ ; v ↦ [S] c fresh
--------------------------------------
-- Γ ; Σ ; accept v ↦ Σ ; Chan c ; c:S
typeExp sigma gamma (EAccept v) = do (_,TD (DSession s),_) <- typeVal sigma gamma v
c <- fresh
return (sigma, Chan c, [(cid c, s)])
-- C-Request
-- Γ ; v ↦ [S] c fresh
---------------------------------------------
-- Γ ; Σ ; accept v ↦ Σ ; Chan c ; c:(dual S)
typeExp sigma gamma (ERequest v) = do (_,TD (DSession s),_) <- typeVal sigma gamma v
c <- trace (printf "SIG: %s :SIG" (show sigma)) $ fresh
return (sigma, Chan c, [(cid c, dual s)])
-- C-App
-- Γ ; v ↦ (Σ ; T ↦ U ; Σ') Γ ; v' ↦ T
-----------------------------------------
-- Γ ; Σ,Σ" ; v v' ↦ Σ" ; U ; Σ'
typeExp sigma gamma (EApp v v') = do (_, TD (DArrow σ t u σ'),_) <- typeVal sigma gamma v
(_,t',_) <- typeVal sigma gamma v'
let σ'' = extractset σ sigma
if t /= t'
then error $ printf "Types for application do not match: %s and %s" (show t) (show t')
else return (σ'', u, σ')
-- C-New
-- Γ ; Σ ; new S ↦ Σ ; [S] ; ∅
typeExp sigma gamma (ENew s) = return (sigma, TD (DSession s), [])
typeExp sigma gamma (ET t) = typeThread sigma gamma t
-- C-Let
-- Γ ; Σ ; e ↦ Σ₁ ; T₁ ; Σ₁' Γ,x:T₁ ; Σ₁,Σ₁' ; t ↦ Σ₂ ; T₂ ; Σ₂'
-------------------------------------------------------------------
-- Γ ; Σ ; let x = e in t ↦ Σ₁ ∩ Σ₂ ; T₂ ; (Σ₁' ∩ Σ₂),Σ'₂
typeThread :: Sigma -> Gamma -> T -> State St (Sigma, Typ, Sigma)
typeThread sigma gamma (TLet x e t) = do (σ1, t1, σ1') <- typeExp sigma gamma e
let gamma' = extend gamma x t1
sigma' = union σ1 σ1'
(σ2, t2, σ2') <- typeThread sigma' gamma' t
return (σ1 `intersect` σ2, t2, (σ1' `intersect` σ2) `union` σ2')
-- C-Fork
-- Γ ; Σ ; t ↦ Σ₁ ; T₁ ; ∅ Γ ; Σ₁ ; t' ↦ Σ₂ ; T₂ ; ∅
--------------------------------------------------------
-- Γ ; Σ ; (fork t ; t') ↦ Σ₂ ; T₂ ; ∅
typeThread sigma gamma (TFork t t') = do (σ1, t1,_) <- typeThread sigma gamma t
(σ2, t2,_) <- typeThread σ1 gamma t'
return (σ2, t2, [])
-- C-Val
-- Γ ; v ↦ T
------------------------
-- Γ ; Σ ; v ↦ Σ ; T ; ∅
typeThread sigma gamma (TV v) = typeVal sigma gamma v
--------------------------------------------------------------------------------
--- TEST INPUTS ----------------------------------------------------------------
--------------------------------------------------------------------------------
-------------
-- Threads --
-------------
-- let x = new End in x
t01 = TLet "x" (ENew SEnd)
(TV (VVar "x"))
-- let x = (λx:Int . x) 5 in x
t02 = TLet
"x"
(EApp (VLambda [] "y" (TD DNum) (ET (TV (VVar "y"))))
(VNum 5))
(TV (VVar "x"))
-- fork (let x = new !Int.?Int.End in (accept x));
-- (let y = new !Int.?Int.End in (request x))
t03 = TFork
(TLet
"s"
(ENew (SSendD DNum (SReceiveD DNum SEnd)))
(TLet
"x"
(EAccept (VVar "s"))
(TV (VVar "x"))))
(TLet
"t"
(ENew (SSendD DNum (SReceiveD DNum SEnd)))
(TLet
"y"
(ERequest (VVar "t"))
(TV (VVar "y"))))
ts = [t01, t02, t03]
-----------------
-- Expressions --
-----------------
-- (rec (x:Num).(λ(∅;y:Num) y)) 5
e01 = EApp v02 (VNum 5)
es = [e01]
------------
-- Values --
------------
-- λ(∅;y:Num) y
v01 = VLambda [] "y" (TD DNum) (ET (TV (VVar "y")))
-- rec (x:Num).(λ(∅;y:Num) y)
v02 = VRec "x" (TD DNum) v01
vs = [v01, v02]
--------------------------------------------------------------------------------
--- MAIN -----------------------------------------------------------------------
--------------------------------------------------------------------------------
main = do print "Threads"
mapM_ (\e -> print $ evalState (typeThread [] [] e) 1) ts
print "Expressions"
mapM_ (\e -> print $ evalState (typeExp [] [] e) 1) es
print "Values"
mapM_ (\e -> print $ evalState (typeVal [] [] e) 1) vs
Raw
Syntax.hs
module Syntax where
-- _ ____ _____
-- / \ / ___|_ _|
-- / _ \ \___ \ | |
-- / ___ \ ___) || |
-- /_/ \_\____/ |_|
data T
= TV V
| TLet String E T
| TFork T T
deriving (Show, Eq)
data E
= ET T
| EApp V V
| ENew S
| EAccept V
| ERequest V
| ESend V V
| EReceive V
| ECase V [(L, E)]
| ESelect L V
| EClose V
deriving (Show, Eq)
data V
= VAlpha Alpha
| VLambda Sigma String Typ E
| VRec String Typ V
| VUnit
| VVar String
| VNum Integer
deriving (Show, Eq)
-- _____
-- |_ _| _ _ __ ___ ___
-- | || | | | '_ \ / _ \/ __|
-- | || |_| | |_) | __/\__ \
-- |_| \__, | .__/ \___||___/
-- |___/|_|
data Alpha
= AId { cid :: String }
| EId P
deriving (Show, Eq)
data P
= Plus
| Minus
deriving (Show, Eq)
data Typ
= TD D
| Chan Alpha
deriving (Show, Eq)
data D
= DSession S
| DArrow Sigma Typ Typ Sigma
| DUnit
| DNum
deriving (Show, Eq)
data S
= SReceiveD D S
| SSendD D S
| SReceiveS S S
| SSendS S S
| SExternal [(L, S)]
| SInternal [(L, S)]
| SEnd
deriving (Show, Eq)
type Sigma = [(String, S)]
type Gamma = [(String, Typ)]
type L = String
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment