# Cyclic Types

18 Nov 2014

As of March 2020, School of Haskell has been switched to read-only mode.

This is an attempt to capture a concept in Haskell that I have been trying to do for a while. Some of the new extensions and type-level hackery seem to help, though I suspect I am not taking advantage of everything I could. Let me know if this can be simplified or if there is a better way.

Functioning code is at the very bottom.

# Type-Cycles

Some datatypes we commonly use are recursive or mutually recursive, leading to what I call a type-cyclic structure where it is possible to traverse back to the original datatype.

This has a type-cycle of 2, even though the data actually is in a cycle of 4:

``````data A = A Int B
data B = B String A
exampleAB = A 1 \$ B "one" \$ A 2 \$ B "two" exampleAB ``````

This has a type-cycle of 1 when using `drop 1`:

``data List a = Cons a (List a) | Nil``

A tree like this has a type-cycle of 1 as you traverse it manually or with a zipper:

``data Tree a = Node a (Tree a) (Tree a) | Leaf a | TNil``

Last example inspired by `Data.Graph` using `Data.Array`. This has a type-cycle of 1.

``````type Graph = Table [Int]
type Table a = Array Int a
nextItems :: Graph -> Int -> [Int]
nextItems = (!)

nextUnsafe :: Graph -> Int -> Int

Repeated applications of `nextUnsafe g` will traverse the graph one-by-one. Though one can imagine a slower traversal. Taking only a single result (unsafe) when multiple or none are possible leads to a type-cycle of 2 when traversing using `outEdge` and `outNode`. This is similar to the concept of using a bipartite double cover to represent a directed graph.

``````nextEdge :: Graph -> Int -> (Int,Int)
nextEdge g i = (i, head \$ g!i)

nextNode :: (Int,Int) -> Int
nextNode = snd``````

# Abstract away

This notion is pretty general and can be captured with the idea that they are categories with n-objects and the traversals are arrows between them. The category diagram can be represented with a multipartite graph. Zippers have abstracted the notion of traversal; we can use the same polymorphic functions to traverse zippers. I wanted to see if I can make the Haskell type system enforce the notion that a type was cyclic.

## Attempt 1 - find cycles

``````class Cycle1 a where
next :: a -> a``````

Not very promising.

``````class Cycle2 a where
type Next a
next :: Cycle2 (Next a) => a -> Next a``````

This is closer, but it doesn't ensure that the cycle returns to the original datatype. Starting at `a` you may go to `b` which then loops along itself. Not satisfying. It seems we need a way to identify a cycle at the type-level; enter type families:

``````data Cycle (n::Nat)
type Counter a = Count (Next a) a 1
type family Count a b n where
Count a b 20 = Void     -- Used to terminate the type-checker
Count b b n = Cycle n
Count a b n = Count (Next a) b (n+1)``````

This seems to have the right capabilities. We can't use a constraint (or can we? let me know) like `class (Counter a ~ Cycle n) => Cycle a where` because we need to have `n` in the class head. Ideally it would not be manually entered by `instance` writers. With a little type in-equality help:

``````type a /=/ b = (a == b) ~ False

class (Counter a /=/ Void) => Cycle3 a where
type Next a
next :: Cycle3 (Next a) => a -> Next a``````

Success! This ensures that a type-cycle exists and is of a set length `n`.

## Attempt 2 - traverse faster

At the moment `next` merely traverses the structure one-by-one. That is fine for 1-cycles, but how can we do `a -> a` hops for 2-cycles, 3-cycles, etc? I could not think of a way to express this properly:

``````data Cycle (n::Nat) = Proxy
class (Cycle3 a, Counter a ~ Cycle n) => CycleN a n
neighbor :: Count n -> a -> a
neighbor n a = foldr (\$) a \$ replicate (natVal n) next``````

So instead we I tried a next typeclass:

``````data Cycle (n::Nat) {-hi-}a {-/hi-}
type Counter a = Count (Next a) a 1
type family Count a b n where
Count b b n = Cycle n {-hi-}b {-/hi-}
Count a b 3 = Void
Count a b n = Count (Next a) b (n+1)
type CyclicN a r n = (Cyclic a
,Cyclic (Next a)
,Cyclic (Next (Next a))
, {-hi-}Counter a ~ Cycle n a {-/hi-},a~r)
class (CyclicN a r n) => Cyc a r n where
neighbor :: {-hi-}a -> a{-/hi-}

instance (a ~ Next (Next (Next a))
,CyclicN a (Next (Next (Next a))) 3) => Cyc a a 3 where
neighbor = next . next . next
instance (a ~ Next (Next a)
,CyclicN a (Next (Next a)) 2)        => Cyc a a 2 where
neighbor = next . next
instance (a~Next a
, CyclicN a (Next a) 1)              => Cyc a a 1 where
neighbor = next``````

This is an improvement. Now we have the capablity to call `next` the proper number of times to produce the right result to hop through our structure.

## Attempt 3 - Functors and Monads, oh my!

Most of these structures are not single-linked, sometimes the natural result is a list, set, `Maybe`, or anything else. Our function should not be `a -> a`, but more like `Functor => a -> f a` and if it wasn't ugly already; we have to add structure to our `Counter` and even more Constraints:

``````data Cycle (n::Nat) b {-hi-}r {-/hi-}
type Counter a = Count (Next a) a 1 {-hi-}((F a) a){-/hi-}
type family Count a b n r where
Count b b n r = Cycle n b r
Count a b 3 r = Void
Count a b n r = Count (Next a) b (n+1) ((F a) r)

class (Counter a /=/ Void, {-hi-}Functor (F a){-/hi-}) => Cyclic a where
type Next a
{-hi-}type F a :: * -> * {-/hi-}
{-hi-}nextSet :: (Cyclic (Next a)) => a -> F a (Next a){-/hi-}
step :: (Cyclic (Next a)) => a -> Next a

type CyclicN a b n r = (Monad (F a),Cyclic a
,Cyclic (Next a)
,Cyclic (Next (Next a))
,Counter a ~ Cycle n b r, b~a)

class (CyclicN a b n r) => Cyc a b n r where
neighbors :: a -> r

instance (CyclicN a e 3 b,b~F a (F c (F d a)),c~Next a,d~Next c,e~Next d) => Cyc a a 3 b where
neighbors = fmap (fmap nextSet . nextSet) . nextSet
instance (CyclicN a d 2 b,{-hi-}b~F a (F c a){-/hi-},c~Next a,d~Next c) => Cyc a a 2 b where
{-hi-}neighbors = fmap nextSet . nextSet{-/hi-}
instance (CyclicN a c 1 b,b~F a a,c~Next a) => Cyc a a 1 b where
neighbors = nextSet``````

Now I'm getting the hang of type-level computation, but it is very ugly. Any way to clean this up? Wait, we're not done yet!

I don't like having results like `Just (Just (Just 2))`. Let's smash them together whenever possible:

``````data Cycle (n::Nat) b (x :: * -> *) xr (f::Bool)
type Counter a = Count (Next a) a 1 ((F a) a) (F a == F (Next a))
type family Count a b n r f where
Count b b n (x r) f     = Cycle n b x (x r) f
Count a b 3 r f         = Void
Count a b n (x r) True  = Count (Next a) b (n+1) (x r) (F a == F (Next a))
Count a b n (x r) False = Count (Next a) b (n+1) (x ((F a) r)) False``````

and

``````class (CyclicN a b n x xr f ) => Cyc a b n x xr f where
neighbors :: a -> xr

instance (CyclicN a e 3 x xr True, Monad x
,xr~F a a,F a ~ F c,F c ~ F d,c~Next a,d~Next c,e~Next d) => Cyc a a 3 x xr True where
neighbors = nextSet >=> nextSet >=> nextSet

instance (CyclicN a d 2 x xr True ,Monad x
,xr~F a a,F a ~ F c ,c~Next a,d~Next c) => Cyc a a 2 x xr True where
neighbors =  nextSet >=> nextSet``````

Now calling `neighbors` smashes together any duplicate `Monads` in a `join`-like fasion.

# Conclusion

The type system can do quite a bit and I'm almost certain I'm doing it wrong. How can this be simpler?

# Functioning Code

``````{-# LANGUAGE TypeFamilies
,DataKinds
,TypeOperators
,ConstraintKinds
,UndecidableInstances
,FlexibleContexts
,MultiParamTypeClasses
,FlexibleInstances
,GeneralizedNewtypeDeriving
,StandaloneDeriving
#-}
import GHC.TypeLits
import Data.Type.Equality
import Data.Word
import Data.Void
import Data.Functor.Identity
import qualified Data.Graph as G
import Data.Array
deriving instance Show a => Show (Identity a)

main :: IO ()
main = do
print \$ "example:                     : " ++ show example
print \$ "step        (Node 2 example) : " ++ show (step (Node 2 example))
print \$ "step \$ step (Node 2 example) : " ++ show (step \$ step (Node 2 example))
print \$ "neighbors   (Node 2 example) : " ++ show (neighbors (Node 2 example))
print \$ "step     (DirNode 2 example) : " ++ show (step (DirNode 2 example))
print \$ "neighbors(DirNode 1 example) : " ++ show (neighbors (DirNode 1 example))
print \$ "step              (2 :: Int) : " ++ show (step (2 :: Int))
print \$ "step \$ step       (2 :: Int) : " ++ show (step \$ step (2 :: Int))
print \$ "neighbors         (2 :: Int) : " ++ show (neighbors (2 :: Int))
print \$ "neighbors   (2,exampleGraph) : " ++ show (neighbors (2::Int,exampleGraph))

exampleGraph = G.buildG (0,2) [(0,1),(1,2),(2,0),(2,1)]

type DList = [(Int,[Int])]
example :: DList
example = [(0,),(1,),(2,[0,1])]

data Node = Node Int DList
instance Show Node where
show (Node x _) = "Node " ++ show x ++ " example"
data DirNode = DirNode Int DList
instance Show DirNode where
show (DirNode x _) = "DirNode " ++ show x ++ " example"
data Edge = Edge (Int,Int) DList
instance Show Edge where
show (Edge x _) = "Edge " ++ show x ++ " example"

newtype L a = L [a] deriving (Show,Functor,Monad) -- No type-level lamdas! gar!
instance Cyclic Node where
type Next Node = Node
type F Node = L
step (Node x xs) = Node (fst (xs !! head (snd (xs !! x)))) xs
nextSet (Node x xs) = L \$ map (\y -> Node y xs) (snd \$ xs !! x)

instance Cyclic DirNode where
type Next DirNode = Edge
type F DirNode = L
step (DirNode x xs) = Edge (x,fst (xs !! head (snd (xs !! x)))) xs
nextSet (DirNode x xs) = L \$ map (\y -> Edge (x,y) xs) (snd (xs !! x))
instance Cyclic Edge where
type Next Edge = DirNode
type F Edge = Identity
step (Edge x xs) = DirNode (snd x) xs
nextSet (Edge x xs) = Identity \$ DirNode (snd x) xs
-- This instance has a cycle, but not one that returns to the original instance
{-
step (BadInstance x xs) = DirNode (fst x) xs
nextSet = Identity . step
---}
instance Cyclic Int where
type Next Int = Integer
type F Int = Identity
step x = 2 * fromIntegral x
nextSet = Identity . step
instance Cyclic Integer where
type Next Integer = Word32
type F Integer = Identity
nextSet = Identity . step
step x = 2 * fromIntegral x
instance Cyclic Word32 where
type Next Word32 = Int
type F Word32 = Identity
step x = 2 * fromIntegral x
nextSet = Identity . step

instance Cyclic [a] where
type Next [a] = [a]
type F [a] = Maybe
step = tail
nextSet (_:x:xs) = Just (x:xs)
nextSet _ = Nothing

data Tree a = TNode a (Tree a) (Tree a) | Leaf a | Nil
instance Cyclic (Tree a) where
type Next (Tree a) = Tree a
type F (Tree a) = L
step (TNode _ a _) = a  -- Can't use Forest without fully applying it! gar!
step _ = Nil
nextSet (TNode _ xs ys) = L [xs,ys]
nextSet _ = L []

instance Cyclic (G.Vertex,G.Graph) where
type Next (G.Vertex,G.Graph) = (G.Edge,G.Graph)
type F (G.Vertex,G.Graph) = L
step (v,g) = ( (v,head \$ g!v) ,g)
nextSet (v,g) = L \$ map (\x -> ( (v,x),g)) \$ g!v

instance Cyclic (G.Edge,G.Graph) where
type Next (G.Edge,G.Graph) = (G.Vertex,G.Graph)
type F (G.Edge,G.Graph) = L
step ((_,v),g) = (v,g)
nextSet ((_,v),g) = L [(v,g)]

-- show
data Cycle (n::Nat) b (x :: * -> *) xr (f::Bool)
type Counter a = Count (Next a) a 1 ((F a) a) (F a == F (Next a))
type family Count a b n r f where
Count b b n (x r) f     = Cycle n b x (x r) f
Count a b 3 r f         = Void
Count a b n (x r) True  = Count (Next a) b (n+1) (x r) (F a == F (Next a))
Count a b n (x r) False = Count (Next a) b (n+1) (x ((F a) r)) False

class (Counter a /=/ Void, Functor (F a),Monad (F a)) => Cyclic a where
type Next a
type F a :: * -> *
nextSet :: (Cyclic (Next a)) => a -> F a (Next a)
step :: (Cyclic (Next a)) => a -> Next a

class (Counter w /=/ Void, Functor (F2 w),Monad (F w)) => Cyclic2 w where
type Part w
type F2 w :: * -> *

type CyclicN a b n x xr f= (Monad (F a),Cyclic a
,Cyclic (Next a)
,Cyclic (Next (Next a))
,Counter a ~ Cycle n b x xr f, b~a)
class (CyclicN a b n x xr f ) => Cyc a b n x xr f where
neighbors :: a -> xr
instance (CyclicN a e 3 x xr True, Monad x
,xr~F a a,F a ~ F c,F c ~ F d,c~Next a,d~Next c,e~Next d) => Cyc a a 3 x xr True where
neighbors = nextSet >=> nextSet >=> nextSet
instance (CyclicN a e 3 x xr False
,xr~F a (F c (F d a)),c~Next a,d~Next c,e~Next d) => Cyc a a 3 x xr False where
neighbors = fmap (fmap nextSet . nextSet) . nextSet

instance (CyclicN a d 2 x xr True ,Monad x
,xr~F a a,F a ~ F c ,c~Next a,d~Next c) => Cyc a a 2 x xr True where
neighbors =  nextSet >=> nextSet
instance (CyclicN a d 2 x xr False
,xr~F a (F c a)      ,c~Next a,d~Next c) => Cyc a a 2 x xr False where
neighbors = fmap nextSet . nextSet

instance (CyclicN a c 1 x xr f
,xr~F a a,c~Next a) => Cyc a a 1 x xr f where
neighbors = nextSet

type a /=/ b = (a == b) ~ False
-- /show``````