{-# LANGUAGE ConstraintKinds           #-}
{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE UndecidableInstances      #-}

{-|

Module      : PolyList
Description : Polymorhic list.
Copyright   : © Frank Jung, 2024
License     : GPL-3.0-only

From [Thinking with
Types](https://github.com/isovector/thinking-with-types), Sandy Maguire,
2021, section 5.3 Heterogeneous Types.

== Source

See [Thinking with Types](https://github.com/isovector/thinking-with-types)
for code and solutions to exercises.

== Unable to Derive Functor for Hetereogeneous Lists

Unfortunately, for your PolyList type, it's not possible to create a Functor
instance because PolyList is indexed by a type-level list of types, and Functor
requires a type constructor of kind @* -> *@, i.e., a type constructor that
takes exactly one type argument.

The PolyList type is a heterogeneous list that can contain values of different
types, and the type of each value is encoded in the type of the list itself.
This is fundamentally different from the concept of a Functor, which operates
on homogeneous containers that contain values of a single type.

See also "RankNTypes" for other examples.

-}

module PolyList
  (
    -- * Types
    PolyList (..)
  , HEntry (..)
    -- * Functions
  , pLength
  , pHead
  ) where

import           Data.Kind (Constraint, Type)

-- | A constraint that applies to all types in a list.
type family All (c :: Type -> Constraint) (ts :: [Type]) :: Constraint where
  All _ '[] = ()
  All c (t : ts) = (c t, All c ts)

-- | A list that contain polymorphic types.
data PolyList (ts :: [Type]) where
  PNil :: PolyList '[]
  (:#) :: t -> PolyList ts -> PolyList (t ': ts)
infixr 5 :#

instance All Eq ts => Eq (PolyList ts) where
  PolyList ts
PNil == :: PolyList ts -> PolyList ts -> Bool
== PolyList ts
PNil           = Bool
True
  (t
a :# PolyList ts
as) == (t
b :# PolyList ts
bs) = t
a t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
t
b Bool -> Bool -> Bool
&& PolyList ts
as PolyList ts -> PolyList ts -> Bool
forall a. Eq a => a -> a -> Bool
== PolyList ts
PolyList ts
bs

instance (All Eq ts, All Ord ts) => Ord (PolyList ts) where
  PolyList ts
PNil compare :: PolyList ts -> PolyList ts -> Ordering
`compare` PolyList ts
PNil         = Ordering
EQ
  compare (t
a :# PolyList ts
as) (t
b :# PolyList ts
bs) = t -> t -> Ordering
forall a. Ord a => a -> a -> Ordering
compare t
a t
t
b  Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> PolyList ts -> PolyList ts -> Ordering
forall a. Ord a => a -> a -> Ordering
compare PolyList ts
as PolyList ts
PolyList ts
bs

instance (All Show ts) => Show (PolyList ts) where
  show :: PolyList ts -> String
show PolyList ts
PNil      = String
"PNil"
  show (t
a :# PolyList ts
as) = t -> String
forall a. Show a => a -> String
show t
a String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" :# " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> PolyList ts -> String
forall a. Show a => a -> String
show PolyList ts
as

-- | Get the length of a polymorphic list.
pLength :: PolyList ts -> Int
pLength :: forall (ts :: [*]). PolyList ts -> Int
pLength PolyList ts
PNil      = Int
0
pLength (t
_ :# PolyList ts
ts) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ PolyList ts -> Int
forall (ts :: [*]). PolyList ts -> Int
pLength PolyList ts
ts

-- | Get the head of a polymorphic list.
pHead :: PolyList (t ': ts) -> t
pHead :: forall t (ts :: [*]). PolyList (t : ts) -> t
pHead (t
t :# PolyList ts
_) = t
t
t

-- | An alternate implementation of a heterogenous item.
-- The 'HEntry' type is an existential wrapper around a value of any type that
-- has a 'Show' instance. This allows us to store values of different types in a
-- list, but we can't derive 'Eq' or 'Ord' for 'HEntry' because the types are
-- potentially different.
--
-- See also "RankNTypes" for other examples.
data HEntry = forall a. Show a => HEntry a

instance Show HEntry where
  show :: HEntry -> String
show (HEntry a
a) = a -> String
forall a. Show a => a -> String
show a
a