Correct
Looping Arrows from Cyclic Terms
Tr a c e d C a t e g o r i c a l I n t e r p r e t a t i o n i n H a s k e l l

Gunma University, Japan

Makoto Hamana

Arrow

Programming
Difficult !
counter :: Automaton Int Int
counter = proc reset -> dorec output <- returnA -<if (reset==1)
then 0 else next
next<- delay 0 -< output+1
returnA -< output▻ Arrow with loop
▻ … is defined recursively

Two kinds of loops
1. Looping computation• Arrow with loop
• Recursive function
2. Looping data
•Haskellʼs recursive definition

clist = 5 : 6 : clist
ctree = let x = (Bin (Bin ctree (Lf 5)) x) in
Bin x (Lf 6)

A common principle exists

T h i s

Ta l kPart I. Show usefulness of a principle
through
３ examples
Part II. Explain a relationship between
abstract semantics andconcrete arrow programming•

Semantics ⇔ ProgramingArrow programmingwith loop

IMethodology

Data structure for Cycles▻ μ-terms▻

can be represented by a μ-term▻ In Haskell, defined bytype Var = Chardata Term = V Var | Mu Var Term | Nil | Cons Int TermclistTm= Mu 'x' (Cons 5 (Cons 6 (V 'x')))3EXAMPLES

1Case I. Cyclic Data Structure▻ HaskellclistTm = Mu 'x' (Cons 5 (Cons 6 (V 'x')))
Challenge 1
Can you generate a truly cyclic list from it？
This means to give a cyclic list defined byclist = 5:6:clist
from a term clistTm without using
destructive updates or meta-programming.

Case II. Circuitspecification

data Term = V Var| Mu Var Term
| Cond Term Term Term

Arrow program
counter :: Automaton Int Int
counter = proc reset -> dorec output <- returnA -<if (reset==1)| Const0| Delay0 Termthen 0 else next
| Inc Termnext<- delay 0 -< output+1| Add Term Term
returnA -< output

counterTm = Mu ‘x’ (Cond (V ‘r’) Const0(Delay0 (Inc (V 'x'))))

Challenge 2Generate an arrow representing this circuit from the term
counterTm without meta-programming

Case III. Recurcrsive Function
Recursive function

fact :: Int -> Intfact 0 = 1
fact n = n * fact (n-1)…See the paperA n s w e r s2

Case I

Cyclic DataStructure

Case I. Cyclic Data Structure
Challenge 1

Can you generate a trulely cyclic list fromMu ‘x’ (Cons 5 (Cons 6 (V ‘x’)))?

▻translation▻ “homomorphic”
Idea：Connect thelast cell and the root
▻ Translationtranstrans :::: Term
Term ->-> [(Var,[Int])][(Var,[Int])] ->-> [Int]
[Int]
trans
ps
trans (V(V x)x)ps == lkup
lkup xx ps
pstransps
trans (Mu(Mu xx t)t)ps == let
let pp == transtrans tt ((x,p):ps)((x,p):ps) inin pptransps
trans NilNil
ps == [][]
transtrans (Cons(Cons aa t)t) ps
ps == aa :: (trans(trans tt ps)ps)▻ lkup
Execution
μ-termʼsμx ((x',n):es)| x == x'= n*Main>'x' (Cons5 (Cons= 6lkup(V 'x'))))[]
lkup transx ( _ (Mu :es)
| otherwise
x es
5:6:5:6:5:6:5:6:5:6:...

Case I. Cyclic Data Structure
Arrow ver.

type A = (->)

tl :: Term -> A [(Var, [Int])] [Int]dup x = (x,x)
tl (V x)= arr (lkup x)
tl (Mu x t)
= loop (arr dup <<< tl t<<< arr (λ(ps,p)->(x,p):ps))tl Nil= arr (λps -> [])tl (Cons a t) = arr (a:) <<< tl t▻arrow combinators(<<<, arr, loop)▻This works for any arrow type A▻Why correct？

Case I. Cyclic Data Structure
Normal version
trans :: Term -> ([(Var,[Int])]->[Int][Int])[(Var,[Int])] ->trans(V x)x) ps =xps
λpsx pstrans (V= lkuplkup->x lkup

Arrow version
tltl::Term -> A [(Var, [Int])] [Int](V x)= arr (lkup x)
when A = (->)
arr f = fCase I. Cyclic Data Structure
Arrow ver.

type A = (->)

tl :: Term -> A [(Var, [Int])] [Int]dup x = (x,x)
tl (V x)= arr (lkup x)
tl (Mu x t)
= loop (arr dup <<< tl t<<< arr (λ(ps,p)->(x,p):ps))tl Nil= arr (λps -> [])tl (Cons a t) = arr (a:) <<< tl t▻arrow combinators(<<<, arr, loop)▻This works for any arrow type A▻Why correct？

Case IICircuit

C a s e

I I .

C i r c u i t

counterTm = Mu 'x' (Cond (V 'r') Const0 (Delay0 (Inc (V 'x'))))

Translation to arrows
tl :: Term -> Automaton [(Var,Int)] Int
tl (V x)= arr (lkup x)
tl (Mu x t) = loop (arr dup <<< tl t <<< arr (λ(ps,p)->(x,p):ps))tl (Const0) = const0 <<< arr (λx->())
tl (Inc t)= inc<<< tl t
tl (Delay0 t)= delay0 <<< tl t
tl (Add s t) = add<<< (tl s) &&& (tl t)
tl (Cond s t u) = cond <<< tl s &&& (tl t &&& tl u)

C a s e

I I .

C i r c u i t

counterTm = Mu 'x' (Cond (V 'r') Const0 (Delay0 (Inc (V 'x'))))
Primitives
const0 :: Automaton () Int
inc:: Automaton Int Int
Generate arrows
counterArr :: Automaton Int Int
counterArr = tl counterTm <<< arrconst0 = arr (const 0)
inc= arr (λx-> x+1)
Original arrow program
counter :: Automaton Int Int
counter = proc reset -> dorec output <- returnA -<if (reset==1)(λn->[('r',n)])then 0 else next
next<- delay 0 -< output+1
returnA -< output

Tests
test_input = [1,0,1,0,0,1,0,1]
runOrig = partrun counter
test_input
runOurs = partrun counterArr test_input
Gives the same signals*Main> runOrig[0,1,0,1,2,0,1,0]-- Original-- Cyclic term ver.

*Main> runOurs[0,1,0,1,2,0,1,0]

Case III

Recursive
Function…See the paper

Case I 〜 IIItl :: Term -> A [(Var,D)] Dtl (V x)= arr (lkup x)tl (Mu x t) = loop (arr dup <<< tl t<<< arr (λ(ps,p)->(x,p):ps))………
Other cases are strateforward translations

Why correct？

Category-theoreticFoundations

IIIntuitions▻Regard an arrow type A x y asa hom-setof some category▻Haskellʼs arrow f :: A x y▻A = (->) The category Hask
▻objects: Haskell types▻arrows: Haskell functions

Semantics of arrows: Freyd categorycartesian[Heunen,Jacobs’08] [Power,Robinson’97]

premonoidal

Freyd cat.

identity-on-objects

Values

Effectfulcomputations

Semantics of arrows: Haskell casecartesianpremonoidalmorphisms= arrows of A

HaskA
Hask
f

arr f

Semantics of Cyclic Structure: Traces[Joyal, Street, Verity’96][Hasegawa’97]

loop = Tr in Haskell

Semantics of arrows with loop
cartesiantracedpremonoidal

morphisms= arrows of A

HaskA
Hask
f

arr f

loop

Case I 〜 III
tl :: Term -> A [(Var,D)] D
tl (V x)= arr (lkup x)
tl (Mu x t) = loop (arr dup <<< tl t<<< arr (λ(ps,p)->(x,p):ps))………
Other cases are strateforward translations

Why correct？

Tra c e d C a t e g o r i c a l I n t e r p r e t a t i o n[Hasegawaʼ97] This interpretation gives fixpoints

term

S ’s morphism

Its arrow version in Haskell

tl (V x)tl (Mu x t)

= arr (lkup x)= loop (arr dup <<< tl t<<< arr(λ(ps,p)->(x,p):ps))Correct Looping Arrows from Cyclic Terms

Tr a c e d C a t e g o r i c a l I n t e r p r e t a t i o n i n H a s k e l l