Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- {-# Language
- DataKinds,
- TypeOperators,
- PolyKinds,
- TypeFamilies,
- UndecidableInstances
- #-}
- data N = Z | S N
- type family Head (xs :: [a]) :: a where
- Head (x ': xs) = x
- type family Drop (n :: N) (xs :: [a]) :: [a] where
- Drop (S n) (x ': xs) = Drop n xs
- Drop Z xs = xs
- type family (!!) (xs :: [a]) (n :: N) :: a where
- (!!) xs n = Head (Drop n xs)
- type SumType (n :: N) (a :: [*]) = a !! n
- type Eg = [Bool,Int,Bool]
- eg :: SumType Z Eg
- eg = False
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement