{-| Module : Lists Description : Different types of lists exploiting type arithmetic Maintainer : gatlin@niltag.net 'Counted' lists have a length represented by a 'Peano' number encoded in their types which permit compile-time bounds checking. The members of 'Conic' lists, meanwhile, do not need to be all of the same type. The type of each list member is encoded in the list's type signature. -} {-# LANGUAGE TypeFamilies, TypeOperators, PolyKinds, DataKinds, RankNTypes #-} {-# LANGUAGE ConstraintKinds, ScopedTypeVariables, FlexibleInstances #-} {-# LANGUAGE ExistentialQuantification, MultiParamTypeClasses #-} module Lists ( -- * Counted Lists Counted(..) , count , unCount -- ** Counted utilities , replicate , append , nth , padTo , zip -- * Conic Lists , Conic(..) , (:-:) , Nil -- ** Type-level conic manipulation , Replicable(type Replicate) , Tackable(type Tack, tack) , HasLength(type Length) -- * Conversion , heterogenize , homogenize ) where import Prelude hiding ( LT , replicate , zip , iterate , take , head , tail , map , repeat , zipWith , take , (-) , (+) , (<=) , (<) ) import qualified Prelude as P import Data.List (intercalate) import Peano ( S , Z , Natural(..) , type (+) , Minus(..) , type (-) , type (<) , type (<=) , ReifyNatural(..)) import Data.Kind (Type) -- = Counted lists infixr 5 ::: -- | A 'Counted' list encodes its length as a type parameter. data Counted (n :: Type) (a :: Type) = forall t. (n ~ S t) => a ::: (Counted t a) -- ^ Prepend an item. | (n ~ Z) => CountedNil -- ^ Construct an empty list. instance Functor (Counted n) where fmap :: forall a b. (a -> b) -> Counted n a -> Counted n b fmap a -> b _ Counted n a CountedNil = forall n a. (n ~ Z) => Counted n a CountedNil fmap a -> b f (a a ::: Counted t a as) = a -> b f a a forall n a t. (n ~ S t) => a -> Counted t a -> Counted n a ::: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap a -> b f Counted t a as instance (ReifyNatural n) => Applicative (Counted n) where pure :: forall a. a -> Counted n a pure = forall n x. Natural n -> x -> Counted n x replicate (forall n. ReifyNatural n => Natural n reifyNatural :: Natural n) Counted n (a -> b) fs <*> :: forall a b. Counted n (a -> b) -> Counted n a -> Counted n b <*> Counted n a xs = forall a b c. (a -> b -> c) -> (a, b) -> c uncurry forall a. a -> a id forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> forall n a b. Counted n a -> Counted n b -> Counted n (a, b) zip Counted n (a -> b) fs Counted n a xs instance (Show x) => Show (Counted n x) where showsPrec :: Int -> Counted n x -> ShowS showsPrec Int p Counted n x xs = Bool -> ShowS -> ShowS showParen (Int p forall a. Ord a => a -> a -> Bool > Int 10) forall a b. (a -> b) -> a -> b $ String -> ShowS showString forall a b. (a -> b) -> a -> b $ forall a. [a] -> [[a]] -> [a] intercalate String " ::: " (forall a b. (a -> b) -> [a] -> [b] P.map forall a. Show a => a -> String show forall a b. (a -> b) -> a -> b $ forall n a. Counted n a -> [a] unCount Counted n x xs ) forall a. [a] -> [a] -> [a] ++ String " ::: CountedNil" instance Eq a => Eq (Counted n a) where Counted n a CountedNil == :: Counted n a -> Counted n a -> Bool == Counted n a CountedNil = Bool True (a h1 ::: Counted t a t1) == (a h2 ::: Counted t a t2) | a h1 forall a. Eq a => a -> a -> Bool == a h2 = Counted t a t1 forall a. Eq a => a -> a -> Bool == Counted t a t2 | Bool otherwise = Bool False -- | Compute the length of a @Counted@ in terms of a @Natural@. count :: Counted n a -> Natural n count :: forall n a. Counted n a -> Natural n count Counted n a CountedNil = forall n. (n ~ Z) => Natural n Zero count (a _ ::: Counted t a xs) = forall n t. (n ~ S t) => Natural t -> Natural n Succ (forall n a. Counted n a -> Natural n count Counted t a xs) unCount :: Counted n a -> [a] unCount :: forall n a. Counted n a -> [a] unCount Counted n a xs = forall n a. Counted n a -> [a] -> [a] go Counted n a xs [] where go :: Counted n a -> [a] -> [a] go :: forall n a. Counted n a -> [a] -> [a] go Counted n a CountedNil [a] final = [a] final go (a x ::: Counted t a xs) [a] acc = forall n a. Counted n a -> [a] -> [a] go Counted t a xs (a x forall a. a -> [a] -> [a] : [a] acc) replicate :: Natural n -> x -> Counted n x replicate :: forall n x. Natural n -> x -> Counted n x replicate Natural n Zero x _ = forall n a. (n ~ Z) => Counted n a CountedNil replicate (Succ Natural t n) x x = x x forall n a t. (n ~ S t) => a -> Counted t a -> Counted n a ::: forall n x. Natural n -> x -> Counted n x replicate Natural t n x x append :: Counted n a -> Counted m a -> Counted (m + n) a append :: forall n a m. Counted n a -> Counted m a -> Counted (m + n) a append Counted n a CountedNil Counted m a ys = Counted m a ys append (a x ::: Counted t a xs) Counted m a ys = a x forall n a t. (n ~ S t) => a -> Counted t a -> Counted n a ::: forall n a m. Counted n a -> Counted m a -> Counted (m + n) a append Counted t a xs Counted m a ys nth :: (n < m) => Natural n -> Counted m a -> a nth :: forall n m a. (n < m) => Natural n -> Counted m a -> a nth Natural n Zero (a a ::: Counted t a _) = a a nth (Succ Natural t n) (a _ ::: Counted t a as) = forall n m a. (n < m) => Natural n -> Counted m a -> a nth Natural t n Counted t a as -- | Pad the length of a list to a given length. -- If the number specified is less than the length of the list given, it won't -- pass the type checker. [^1] padTo :: (m <= n) => Natural n -> x -> Counted m x -> Counted ((n - m) + m) x padTo :: forall m n x. (m <= n) => Natural n -> x -> Counted m x -> Counted ((n - m) + m) x padTo Natural n n x x Counted m x list = Counted m x list forall n a m. Counted n a -> Counted m a -> Counted (m + n) a `append` forall n x. Natural n -> x -> Counted n x replicate (Natural n n forall x y. (Minus x y, LessThanOrEqual y x ~ 'True) => Natural x -> Natural y -> Natural (x - y) `minus` forall n a. Counted n a -> Natural n count Counted m x list) x x zip :: Counted n a -> Counted n b -> Counted n (a, b) zip :: forall n a b. Counted n a -> Counted n b -> Counted n (a, b) zip (a a ::: Counted t a as) (b b ::: Counted t b bs) = (a a, b b) forall n a t. (n ~ S t) => a -> Counted t a -> Counted n a ::: forall n a b. Counted n a -> Counted n b -> Counted n (a, b) zip Counted t a as Counted t b bs zip Counted n a CountedNil Counted n b _ = forall n a. (n ~ Z) => Counted n a CountedNil -- = Conic lists infixr 5 :-: data (x :: k1) :-: (y :: k2) data Nil -- | Conic lists are lists where each element is an @f a@ for some @a@, but the -- @a@ may be different for each element. -- Types of elements are kept track of in the type list. data Conic f ts = forall rest a. (ts ~ (a :-: rest)) => (f a) :-: (Conic f rest) | (ts ~ Nil) => ConicNil class ReifyNatural n => Replicable n (x :: k) where type Replicate n x :: Type instance Replicable Z x where type Replicate Z x = Nil instance Replicable n x => Replicable (S n) x where type Replicate (S n) x = x :-: Replicate n x -- | A @Conic@ length may be computed at the type level. class HasLength (ts :: k) where type Length ts :: Type instance HasLength Nil where type Length Nil = Z instance HasLength (x :-: xs) where type Length (x :-: xs) = S (Length xs) -- | A @Conic@ supports "tacking" a value onto its head. class Tackable (x :: k) (xs :: Type) where type Tack x xs :: Type tack :: f x -> Conic f xs -> Conic f (Tack x xs) instance Tackable a Nil where type Tack a Nil = a :-: Nil tack :: forall (f :: k -> *). f a -> Conic f Nil -> Conic f (Tack a Nil) tack f a a Conic f Nil ConicNil = f a a forall {k} (f :: k -> *) ts rest (a :: k). (ts ~ (a :-: rest)) => f a -> Conic f rest -> Conic f ts :-: forall {k} (f :: k -> *) ts. (ts ~ Nil) => Conic f ts ConicNil instance Tackable a xs => Tackable a (x :-: xs) where type Tack a (x :-: xs) = x :-: Tack a xs tack :: forall (f :: k -> *). f a -> Conic f (x :-: xs) -> Conic f (Tack a (x :-: xs)) tack f a a (f a x :-: Conic f rest xs) = f a x forall {k} (f :: k -> *) ts rest (a :: k). (ts ~ (a :-: rest)) => f a -> Conic f rest -> Conic f ts :-: forall k (x :: k) xs (f :: k -> *). Tackable x xs => f x -> Conic f xs -> Conic f (Tack x xs) tack f a a Conic f rest xs -- = Conversion -- | Turned a 'Counted' list into a 'Conic' list by means of some function from -- @a@ to @(f t)@. heterogenize :: (a -> f t) -> Counted n a -> Conic f (Replicate n t) heterogenize :: forall {k} a (f :: k -> *) (t :: k) n. (a -> f t) -> Counted n a -> Conic f (Replicate n t) heterogenize a -> f t _ Counted n a CountedNil = forall {k} (f :: k -> *) ts. (ts ~ Nil) => Conic f ts ConicNil heterogenize a -> f t f (a x ::: Counted t a xs) = a -> f t f a x forall {k} (f :: k -> *) ts rest (a :: k). (ts ~ (a :-: rest)) => f a -> Conic f rest -> Conic f ts :-: forall {k} a (f :: k -> *) (t :: k) n. (a -> f t) -> Counted n a -> Conic f (Replicate n t) heterogenize a -> f t f Counted t a xs -- | Given a function to collapse any @(f t)@, turn a 'Conic' list into a -- 'Counted' list. homogenize :: (forall t. f t -> a) -> Conic f ts -> Counted (Length ts) a homogenize :: forall {k} (f :: k -> *) a ts. (forall (t :: k). f t -> a) -> Conic f ts -> Counted (Length ts) a homogenize forall (t :: k). f t -> a _ Conic f ts ConicNil = forall n a. (n ~ Z) => Counted n a CountedNil homogenize forall (t :: k). f t -> a f (f a x :-: Conic f rest xs) = forall (t :: k). f t -> a f f a x forall n a t. (n ~ S t) => a -> Counted t a -> Counted n a ::: forall {k} (f :: k -> *) a ts. (forall (t :: k). f t -> a) -> Conic f ts -> Counted (Length ts) a homogenize forall (t :: k). f t -> a f Conic f rest xs {- [^1]: If @padTo@ has the following simpler type ... @ padTo :: (m <= n) => Natural n -> x -> Counted m x -> Counted n x @ ... then GHC reports the following error: @ src/Lists.hs:124:3: error: • Could not deduce: ((n - m) + m) ~ n from the context: m <= n bound by the type signature for: padTo :: forall m n x. (m <= n) => Natural n -> x -> Counted m x -> Counted n x at src/Lists.hs:(117,1)-(122,16) ‘n’ is a rigid type variable bound by the type signature for: padTo :: forall m n x. (m <= n) => Natural n -> x -> Counted m x -> Counted n x at src/Lists.hs:(117,1)-(122,16) Expected type: Counted n x Actual type: Counted ((n - m) + m) x • In the expression: list `append` replicate (n `minus` count list) x In an equation for ‘padTo’: padTo n x list = list `append` replicate (n `minus` count list) x • Relevant bindings include list :: Counted m x (bound at src/Lists.hs:123:11) n :: Natural n (bound at src/Lists.hs:123:7) padTo :: Natural n -> x -> Counted m x -> Counted n x (bound at src/Lists.hs:123:1) | 124 | list `append` replicate (n `minus` count list) x | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ @ I am not entirely certain why the type checker cannot deduce @((n - m) + m) ~ n@, but it cannot and so the type spells out this relation explicitly: @ padto :: (m <= n) => Natural n -> x -> Counted m x -> Counted ((n - m) + m) x @ -}