Vec.hs

{-# LANGUAGE DataKinds, StandaloneKindSignatures, GADTs,
             StandaloneDeriving, DerivingStrategies, ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Wno-unticked-promoted-constructors -Wno-unused-imports #-}

module Vec where

{- 
  Modified by Clinton Mead (clintonmead@gmail.com) to incorporate "runtime" length vectors.

  Original by Richard Eisenberg at https://github.com/goldfirere/video-resources/tree/main/2021-04-20-vectors
  Video discussing at https://www.youtube.com/watch?v=WHeBxSBY0fc

  Note that we've had to complicate the data structures and the interface to handle a mix of
  compile time and runtime vectors.

  Two questions:

  1. Is there a nicer way to do this in Haskell?
  2. Is there a nicer way to do this in a dependently typed language, e.g. Idris?

  And perhaps a bonus question (probably for Richard Eisenberg himself)

  3. How would this be implemented nicely in Haskell if you added your preferred syntax for dependent types?
-}

import Data.Kind ( Type )
import Prelude ( Bool(..), Show, (&&), error, Int, Num ((+), (-)))

{- This file contains most of the functions from Data.List, sorted
   in order of difficulty for implementing these on length-indexed
   vectors. We'll attempt a few each week, getting successively
   harder.
   For documentation, see
   https://hackage.haskell.org/package/base-4.15.0.0/docs/Data-List.html
-}

data Nat = Zero | Succ Nat | Unknown

type Vec :: Nat -> Type -> Type
data Vec n a where
  Nil  :: Vec Zero a
  (:>) :: a -> Vec n a -> Vec (Succ n) a
  Runtime :: Vec m a -> Vec Unknown a

infixr 5 :>

deriving stock instance Show a => Show (Vec n a)

{-
-- these are pretty straightforward:
and
-}

and :: Vec n Bool -> Bool
and Nil = True
and (b :> bs) = b && and bs
and (Runtime vec) = and vec

{-
or
any
all
sum
product
maximum
minimum
foldl
foldl'
foldl1
foldl1'
foldr
foldr1
scanl
scanl'
scanl1
scanr
scanr1
isPrefixOf
isSuffixOf
isInfixOf
isSubsequenceOf
elem
notElem
lookup
find
-- these are a little harder:
head
-}

head :: Vec (Succ n) a -> a
head (x :> _) = x

{-
tail
init
-}

init :: Vec (Succ n) a -> Vec n a
init (_ :> Nil)         = Nil
init (x :> xs@(_ :> _)) = x :> init xs
init (_ :> Runtime Nil) = Runtime Nil 
init (x :> Runtime yl@(_ :> _)) = Runtime (x :> init yl)
init (x :> Runtime (Runtime y)) = init (x :> Runtime y)

{-
last
uncons
singleton
map
-}

map :: (a -> b) -> Vec n a -> Vec n b
map _ Nil       = Nil
map f (x :> xs) = f x :> map f xs
map f (Runtime xs) = Runtime (map f xs)

{-
zip
unzip
zipWith
reverse
mapAccumL
mapAccumR
insert
sort
null
length
-}

type SNat :: Nat -> Type
data SNat n where
  SZero :: SNat Zero
  SSucc :: SNat n -> SNat (Succ n)
  SRuntime :: Int -> SNat Unknown

-- x :: SNat (Succ (Succ Zero))
-- x must be SSucc (SSucc SZero)

length :: forall n a. Vec n a -> SNat n
length Nil = SZero
length (_ :> xs) = SSucc (length xs)
length (Runtime xs) = SRuntime (lengthInt xs)

lengthInt :: forall n a. Vec n a -> Int
lengthInt Nil = 0
lengthInt (_ :> xs) = 1 + lengthInt xs
lengthInt (Runtime xs) = lengthInt xs

{-
replicate
-}

replicate :: SNat n -> a -> Vec n a
-- replicate :: foreach (n :: Nat) -> a -> Vec n a
replicate SZero _ = Nil
replicate (SSucc n) x = x :> replicate n x
replicate (SRuntime 0) _ = Runtime Nil
replicate (SRuntime n) x = Runtime (x :> replicate (SRuntime (n - 1)) x)

replicateInt :: Int -> a -> Vec Unknown a
replicateInt n = replicate (SRuntime n)

runTimeVec :: Vec Unknown Bool
runTimeVec = replicateInt 3 True

-- This vector has "compileTime" and "runTime" components. We know it contains at least two elements.
mixedVec :: Vec (Succ (Succ Unknown)) Bool
mixedVec = True :> True :> runTimeVec

-- This will typecheck because we know the Vec has at least two elements (so the resulting Vec has at least 0.)
validVec :: Vec Unknown Bool
validVec = init (init mixedVec)

validVec2 :: Vec (Succ Unknown) Bool
validVec2 = init mixedVec

-- This doesn't typecheck because we can't be sure 'runTimeVec' isn't empty.
--invalidVec = init (init (init mixedVec))

{-
(++)
take
drop
stripPrefix
splitAt
concat
-- these need fancy type families (quite hard):
intersperse
inits
tails
intercalate
subsequences
permutations
transpose
-- these need existentials:
concatMap
unfoldr
takeWhile
dropWhile
dropWhileEnd
filter
nub
delete
(\\)
union
intersect
-- these need Fin:
(!!)
elemIndex
elemIndices
findIndex
findIndices
-- these need custom GADTs to encode the right conditions:
span
break
partition
group
-}

{-
The functions listed here we will not attempt.
-- these are not illuminating:
zip3
zip4
zip5
zip6
zip7
zipWith3
zipWith4
zipWith5
zipWith6
zipWith7
unzip3
unzip4
unzip5
unzip6
unzip7
-- these are really about text, not about lists:
lines
words
unlines
unwords
-- these are straightforward generalizations:
nubBy
deleteBy
deleteFirstsBy
unionBy
intersectBy
groupBy
sortBy
insertBy
maximumBy
minimumBy
genericLength
genericTake
genericDrop
genericSplitAt
genericIndex
genericReplicate
sortOn
-- no infinite vectors:
no iterate
no iterate'
no repeat
no cycle
-}