Advertisement
Guest User

Untitled

a guest
Apr 23rd, 2019
149
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. {-# Language GADTSyntax,ExistentialQuantification,TypeOperators,PolyKinds,DataKinds,TypeFamilies,TypeInType #-}
  2.  
  3. import GHC.Exts
  4.  
  5. type family State (x :: * -> * -> *) :: Constraint where
  6.  State Basecase = ()
  7.  State (Nested xs) = ()
  8.  
  9. data Basecase s a where
  10.  Stream' :: Stream s a -> Basecase s a
  11. Linear' :: Linear s a -> Basecase s a
  12.  Stack'  :: Stack  s a -> Basecase s a
  13.  
  14. data Stream s a = Stream (a,s)
  15.  
  16. data Linear s a = Linear (a,s) | End a
  17.  
  18. data Stack  s a = Stack  (a,s) | Empty
  19.  
  20. type family Head (xs :: [a]) :: a where
  21. Head (x ': xs) = x
  22.  
  23. data Nested (xs :: [* -> * -> *]) (s :: *) (a :: *) where
  24.  Nested :: (State x,Head xs ~ x) => x s a -> Nested xs s a
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement