Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- {-# Language GADTSyntax,ExistentialQuantification,TypeOperators,PolyKinds,DataKinds,TypeFamilies,TypeInType #-}
- import GHC.Exts
- type family State (x :: * -> * -> *) :: Constraint where
- State Basecase = ()
- State (Nested xs) = ()
- data Basecase s a where
- Stream' :: Stream s a -> Basecase s a
- Linear' :: Linear s a -> Basecase s a
- Stack' :: Stack s a -> Basecase s a
- data Stream s a = Stream (a,s)
- data Linear s a = Linear (a,s) | End a
- data Stack s a = Stack (a,s) | Empty
- type family Head (xs :: [a]) :: a where
- Head (x ': xs) = x
- data Nested (xs :: [* -> * -> *]) (s :: *) (a :: *) where
- Nested :: (State x,Head xs ~ x) => x s a -> Nested xs s a
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement