Keegan McAllister gave a very nice talk at Boston Haskell last night about &quot;First Class Concurrency&quot;. His slides are available online at <br><br><a href="http://t0rch.org/" target="_blank">http://t0rch.org/</a><br>

<br>His final few slides covered the Pi calculus:<br><br><a href="http://en.wikipedia.org/wiki/Pi_calculus">http://en.wikipedia.org/wiki/Pi_calculus</a><br><br>I took a few minutes over lunch to dash out a finally tagless version of the pi calculus interpreter presented by Keegan, since the topic of how much nicer it would look in HOAS came up during the meeting. <br>

<br>For more information on finally tagless encodings, see: <br><br><a href="http://www.cs.rutgers.edu/%7Eccshan/tagless/jfp.pdf" target="_blank">http://www.cs.rutgers.edu/~ccshan/tagless/jfp.pdf</a><br><br>Of course, Keegan went farther and defined an encoding of the lambda calculus into the pi calculus, but I leave that as an exercise for the reader. ;)<br>
<br>-Edward Kmett<br>

<br>&gt; {-# LANGUAGE Rank2Types, TypeFamilies, FlexibleInstances #-}<br>&gt; module Pi where<br><br>&gt; import Control.Applicative<br>&gt; import Control.Concurrent<br><br>A finally tagless encoding of the Pi calculus. Symantics is a portmanteau of Syntax and Semantics.<br>


<br>&gt; class Symantics p where<br>&gt;     type Name p :: *<br>&gt;     new :: (Name p -&gt; p) -&gt; p<br>&gt;     out :: Name p -&gt; Name p -&gt; p -&gt; p <br>&gt;     (|||) :: p -&gt; p -&gt; p <br>&gt;     inn :: Name p -&gt; (Name p -&gt; p) -&gt; p <br>


&gt;     rep :: p -&gt; p <br>&gt;     nil :: p<br>&gt;     embed :: IO () -&gt; p<br><br>Type level fixed points<br><br>&gt; newtype Nu f = Nu { nu :: f (Nu f) }
 <br><br>&gt; fork :: IO () -&gt; IO () <br>&gt; fork a = forkIO a 
&gt;&gt; return ()<br><br>&gt; forever :: IO a -&gt; IO a<br>&gt; 
forever p = p &gt;&gt; forever p<br><br>
Executable semantics<br>
<br>&gt; instance Symantics (IO ()) where<br>&gt;     type Name (IO ()) =
 Nu Chan<br>&gt;     new f = Nu &lt;$&gt; newChan &gt;&gt;= f<br>&gt;    
 a ||| b = forkIO a &gt;&gt; fork b<br>&gt;     inn (Nu x) f = readChan x
 &gt;&gt;= fork . f<br>&gt;     out (Nu x) y b = writeChan x y &gt;&gt; b<br>&gt;    
 rep = forever <br>&gt;     nil = return ()<br>&gt;     embed = id<br><br>A closed pi calculus term<br><br>&gt; newtype Pi = Pi { runPi :: forall 
a. Symantics a =&gt; a }<br><br>&gt;
 run :: Pi -&gt; IO ()<br>&gt; run (Pi a) = a<br><br>&gt; example = Pi 
(new $ \z -&gt; (new $ \x -&gt; out x z nil <br>&gt;                                   
 ||| (inn x $ \y -&gt; out y x $ inn x $ \ y -&gt; nil))<br>&gt;                  
 ||| inn z (\v -&gt; out v v nil))<br>
<br>A pretty printer for the pi calculus<br><br>&gt; newtype Pretty = Pretty { runPretty :: [String] -&gt; Int -&gt; ShowS } <br>&gt; <br>&gt; instance Symantics Pretty where<br>&gt;     type Name Pretty = String<br>&gt;     new f = Pretty $ \(v:vs) n -&gt; <br>


&gt;         showParen (n &gt; 10) $ <br>&gt;             showString &quot;nu &quot; . showString v . showString &quot;. &quot; . <br>&gt;             runPretty (f v) vs 10<br>&gt;     out x y b = Pretty $ \vs n -&gt; <br>


&gt;         showParen (n &gt; 10) $ <br>&gt;             showString x . showChar &#39;&lt;&#39; . showString y . showString &quot;&gt;. &quot; . <br>&gt;             runPretty b vs 10 <br>&gt;     inn x f = Pretty $ \(v:vs) n -&gt;<br>


&gt;         showParen (n &gt; 10) $<br>&gt;             showString x . showChar &#39;(&#39; . showString v . showString &quot;). &quot; .<br>&gt;             runPretty (f v) vs 10 <br>&gt;     p ||| q = Pretty $ \vs n -&gt; <br>


&gt;         showParen (n &gt; 4) $<br>&gt;             runPretty p vs 5 . <br>&gt;             showString &quot; | &quot; .<br>&gt;             runPretty q vs 4<br>&gt;     rep p = Pretty $ \vs n -&gt; <br>&gt;         showParen (n &gt; 10) $<br>


&gt;             showString &quot;!&quot; .<br>&gt;             runPretty p vs 10<br>&gt;     nil = Pretty $ \_ _ -&gt; showChar &#39;0&#39;<br>&gt;     embed io = Pretty $ \_ _ -&gt; showString &quot;{IO}&quot;<br><br>&gt; instance Show Pi where<br>


&gt;     showsPrec n (Pi p) = runPretty p
 vars n<br>&gt;         where<br>&gt;             vars = fmap return vs 
++ <br>&gt;                    [i : show j | j &lt;- [1..], i &lt;- vs] 
where <br>&gt;             vs = [&#39;a&#39;..&#39;z&#39;]<br><br>Pi&gt; example<br>nu a. (nu b. (b&lt;a&gt;. 0 | b(c). c&lt;b&gt;. b(d). 0) | a(b). b&lt;b&gt;. 0)<br>