Skip to content

Instantly share code, notes, and snippets.

@jFransham
Created September 28, 2016 12:01
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save jFransham/fb93362650581b957381eddf5c8dde73 to your computer and use it in GitHub Desktop.
Save jFransham/fb93362650581b957381eddf5c8dde73 to your computer and use it in GitHub Desktop.
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
data Z
data S n
type family Pred n
type instance Pred (S n) = n
newtype Vec n a = Vec {
foldV' :: forall u. forall b.
u Z b ->
(forall k. a ->
u k b ->
u (S k) b) ->
u n b
}
newtype Const n a = C { unC :: a }
c2 = C . C
unC2 = unC . unC
foldCV z c = unC . foldV (C z) (\x (C xs) -> C $ c x xs)
foldV ::
u Z b ->
(forall k. a ->
u k b ->
u (S k) b) ->
Vec n a -> u n b
foldV z c v = foldV' v z c
nilV = Vec $ \z c -> z
consV :: a -> Vec n a -> Vec (S n) a
consV a v = Vec $ \z c -> c a (foldV z c v)
(@:) = consV
infixr @:
newtype TailV n a = TailV { unwrapTV :: (Vec (Pred n) a, Vec n a) }
tailV :: Vec (S n) a -> Vec n a
tailV = fst . unwrapTV . foldV (TailV (undefined, nilV)) step
where
step :: a -> TailV k a -> TailV (S k) a
step x (TailV (_, xs)) = TailV (xs, x `consV` xs)
headV :: Vec (S n) a -> a
headV = foldCV undefined const
unconsV v = (headV v, tailV v)
instance Show a => Show (Vec n a) where
show = unC2 . foldV (c2 "nilV") (\x xs -> c2 $ show x ++ " @: " ++ unC2 xs)
main :: IO ()
main = putStrLn . show . unconsV $ 1 @: 2 @: 3 @: 4 @: nilV
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment