{-|
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
@
-}