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) | NilA 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 | TNilLast 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
nextUnsafe g = head.(nextItems g)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 = sndAbstract 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 -> aNot very promising.
class Cycle2 a where
type Next a
next :: Cycle2 (Next a) => a -> Next aThis 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 aSuccess! 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) nextSo 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 = nextThis 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 = nextSetNow 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)) Falseand
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 >=> nextSetNow 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
,GADTs
,UndecidableInstances
,FlexibleContexts
,MultiParamTypeClasses
,FlexibleInstances
,GeneralizedNewtypeDeriving
,StandaloneDeriving
#-}
import GHC.TypeLits
import Data.Type.Equality
import Data.Word
import Data.Void
import Data.Functor.Identity
import Control.Monad ((>=>))
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]),(1,[2]),(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
{-
data BadInstance = BadInstance (Int,Int) GList deriving Show
instance Cyclic BadInstance where
type Next BadInstance = DirNode
type F BadInstance = Identity
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