vector.hs

{-# LANGUAGE
  DataKinds
, TypeApplications
, TypeFamilies
, TypeOperators
, TypeInType
, KindSignatures
, ExistentialQuantification
, InstanceSigs
, ScopedTypeVariables
#-}
import Prelude hiding (head, tail, map, replicate, concatMap)
import qualified Data.List as L
import Data.Maybe
import Control.Applicative
import GHC.Types (Type)
import GHC.TypeLits
import Data.Proxy

newtype VList (n :: Nat) (a :: Type) = VList { getVList :: [a] }

instance Eq a => Eq (VList n a) where
  VList xs == VList ys = xs == ys

instance Show a =>  Show (VList n a) where
  show (VList xs) = show xs

-- ugh need singletons here
-- mkVList :: forall n m a. (KnownNat n) => [a] -> VList n a
-- mkVList xs = case fromJust (someNatVal (fromIntegral (L.length xs))) of
--                SomeNat proxy -> VList xs :: VList n a

-- foo = mkVList [1,2,3]

-- DOES NOT TYPECHECK
-- fromList = L.foldr cons nil

nil :: VList 0 a
nil = VList []

cons :: a -> VList n a -> VList (n+1) a
cons x (VList ys) = VList (x:ys)

head :: (CmpNat n 0 ~ 'GT) => VList n a -> a
head (VList xs) = L.head xs

tail :: (CmpNat n 0 ~ 'GT) => VList n a -> VList (n-1) a
tail (VList xs) = VList (L.tail xs)

map :: (a -> b) -> VList n a -> VList n b
map f (VList xs) = VList (L.map f xs)

replicate :: KnownNat n => Proxy n -> a -> VList n a
replicate n a = VList (L.replicate (fromIntegral (natVal n)) a)

concat :: (o ~ (n * m)) => VList m (VList n a) -> VList o a
concat (VList xss) = VList (L.concatMap getVList xss)

concatMap :: (o ~ (n * m))
          => (a -> VList m b) -> VList n a -> VList o b
concatMap = flip bindVL

instance KnownNat n => Functor (VList n) where
  fmap = map

pureVL :: forall n a. KnownNat n => a -> VList n a
pureVL x = replicate (undefined :: Proxy n) x

-- The standard definitions for <*> and >>= in the list monad
-- are ill typed if you do not allow the length index to vary...

apVL :: (o ~ (n * m))
     => VList n (a -> b)
     -> VList m a
     -> VList o b
apVL (VList fs) (VList xs) = VList (fs <*> xs) --  (getZipList (ZipList fs <*> ZipList xs))

-- this type is probably wrong
bindVL :: (o ~ (n * m))
       => VList n a
       -> (a -> VList m b)
       -> VList o b
bindVL (VList xs) f = VList (xs >>= getVList . f)

-- instance KnownNat n => Applicative (VList n) where
--   pure x = replicate (undefined :: Proxy n) x
--   (<*>) :: (KnownNat m, KnownNat o, o ~ (m GHC.TypeLits.* n))
--         => VList n (a -> b)
--         -> VList m a
--         -> VList o b
--   (VList fs) <*> (VList xs) = VList (fs <*> xs) --  (getZipList (ZipList fs <*> ZipList xs))

-- instance KnownNat n => Monad (VList n) where
--   return = pure

--   (VList xs) >>= f =

--------------------------------------------------------------------------------
-- | TESTS
--------------------------------------------------------------------------------

-- good, this fails
--test0 = tail nil

test1 = tail (cons 1 nil)

-- good, this fails as well
--test2 = head (tail (consVL 1 nilVL))

-- Inferred: VList 12 Int
test3 = concatMap (\x -> VList [x, x+1, x+2] :: VList 3 Int)
                 (VList [10,20,30,40] :: VList 4 Int)

--     • Couldn't match type ‘11’ with ‘12’
--         arising from a use of ‘concatMap’
--     • In the expression:
--         concatMap
--           (\ x -> VList [x, x + 1, ....] :: VList 3 Int)
--           (VList [10, 20, 30, 40] :: VList 4 Int)
--       In an equation for ‘test4’:
--           test4
--             = concatMap
--                 (\ x -> VList [x, ....] :: VList 3 Int)
--                 (VList [10, 20, 30, ....] :: VList 4 Int)
-- Failed, modules loaded: none.
-- test4 :: VList 11 Int
-- test4 = concatMap (\x -> VList [x, x+1, x+2] :: VList 3 Int)
--                  (VList [10,20,30,40] :: VList 4 Int)


-- <interactive>:91:10: error:
--     • Couldn't match type ‘0’ with ‘12’
--       Expected type: VList 12 Int
--         Actual type: VList 0 Int
--     • In the second argument of ‘(==)’, namely ‘test1’
--       In the expression: test3 == test1
--       In an equation for ‘it’: it = test3 == test1
-- testEq = test1 == test3