{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | The idea is to create a world of Haskell types, called a Universe. Then to
--   define a 'class' whose methods are only applicable to that set of types. We define
--   a closed set by defining an indexed type constructor Rep. If (Singleton Rep), then it must
--   be that every value of type (Rep t) has exactly 0 or 1 inhabitants. (Rep t) has exactly
--   1 inhabitant if 't' is in the universe, and 0 inhabitants if it is not in the universe.
--   A closely related class is (Indexed s t). We would like a total ordering on (t i) and (t j),
--   where the indices, i and j, are different. We do this by ensuring every value of type (t i)
--   has a unique Shape, and that the type Shape has a total order. Every closed singleton can
--   be totally ordered this way. Other indexed types are used to make well-type terms. I.e.
--   Indexed s t => Exp t, denotes a Haskell data type Exp, related to the type t.
--   Note, unlike singletons, there may not be a unique value of type (Exp t), but there may be
--   a unique Shape for every value.
module Data.Universe (
  Shaped (..),
  Singleton (..),
  Universe (..),
  Any (..),
  Some (..),
  Dyn (..),
  Shape (..),
  Eql,
  (:~:) (Refl),
  TypeRep,
  compareByShape,
)
where

import Data.Kind (Type)
import Data.Type.Equality (TestEquality (..), (:~:) (Refl))
#if __GLASGOW_HASKELL__ < 906
import Type.Reflection (TypeRep, pattern App, pattern Con, pattern Fun)
#else
-- Ghc-9.6 removed the Fun constructor.
import Type.Reflection (TypeRep, pattern App, pattern Con)
#endif

-- ==================================================

-- | Type synonym, so we can use ( :~: ) without TypeOperators
type Eql x y = x :~: y

-- | Given (Singleton T), a value of type (T i) has exactly 0 or 1 inhabitants,
--   so we can compare the structure of the type to get proofs that the indexes (i and j)
--   are the same type, using testEql, at runtime. 'cmpIndex', it is like 'compare'
--   except we can have two different indexes ('a' and 'b').
class Singleton t where
  testEql :: t i -> t j -> Maybe (i :~: j)
  cmpIndex :: t a -> t b -> Ordering

-- | For some indexed types, we can assign a unique Shape to each type,
--   using: 'shape' :: t i -> Shape s   (where s is some Singleton type)
--   the class (Shaped t s) means we can assign a unique Shape to each
--   value of type (t i). Not quite as strong as having a unique inhabitant.
--   Every closed singleton type can be shaped, and many other indexed types
--   can be shaped as well.
class Shaped t rep where
  shape :: t i -> Shape rep

-- | Order two indexed types by their Shape. This is usefull for making (Singleton t)
--   instances when we have (Shaped t r) instances, as cmpIndex can be compareByShape.
compareByShape ::
  forall (rep :: Type -> Type) (t :: Type -> Type) (i :: Type) (j :: Type).
  Shaped t rep =>
  t i ->
  t j ->
  Ordering
compareByShape :: forall (rep :: * -> *) (t :: * -> *) i j.
Shaped t rep =>
t i -> t j -> Ordering
compareByShape t i
x t j
y = forall a. Ord a => a -> a -> Ordering
compare (forall {k} (t :: k -> *) (rep :: * -> *) (i :: k).
Shaped t rep =>
t i -> Shape rep
shape @t @rep t i
x) (forall {k} (t :: k -> *) (rep :: * -> *) (i :: k).
Shaped t rep =>
t i -> Shape rep
shape @t @rep t j
y)

-- | A minimal class of operations defined on the universe described by 'rep' .
--   Feel free to make your own Universe classes with additional methods
class Singleton rep => Universe rep t where
  repOf :: rep t

-- ======================================================================
-- A number of types that existentially quantify (i.e. hide) a type index
-- Each one adding more detail, so that the types can do more

-- | Hide the index for any indexed type 't'
data Any t where
  Any :: t i -> Any t

deriving instance (forall i. Show (t i)) => Show (Any t)

-- | Hide the index for a singleton type 't'
data Some t where
  Some :: Singleton t => t i -> Some t

data Dyn rep where
  Dyn :: Singleton t => t i -> i -> Dyn t

-- ==============================================================================

-- A Shape is a mechanism to define Ord instances for (Some R) where R is an indexed type.
-- Let R be an indexed type, so we have values of types like (R Int), (R [Bool]) etc.  We
-- exploit the fact that some indexed types have a unique Shape for every value of type (R i).
-- We assign this unique Shape using :  shape:: R t -> Shape x.
data Shape rep where
  Nullary :: Int -> Shape rep
  Nary :: Int -> [Shape rep] -> Shape rep
  Esc :: (Singleton rep, Ord t) => rep t -> t -> Shape rep

instance Ord (Shape rep) where
  compare :: Shape rep -> Shape rep -> Ordering
compare (Nullary Int
i) (Nullary Int
j) = forall a. Ord a => a -> a -> Ordering
compare Int
i Int
j
  compare (Nullary Int
_) Shape rep
_ = Ordering
LT
  compare Shape rep
_ (Nullary Int
_) = Ordering
GT
  compare (Nary Int
n [Shape rep]
xs) (Nary Int
m [Shape rep]
ys) = forall a. Ord a => a -> a -> Ordering
compare (Int
n, [Shape rep]
xs) (Int
m, [Shape rep]
ys)
  compare (Nary Int
_ [Shape rep]
_) Shape rep
_ = Ordering
LT
  compare Shape rep
_ (Nary Int
_ [Shape rep]
_) = Ordering
GT
  compare (Esc rep t
r1 t
t1) (Esc rep t
r2 t
t2) =
    case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql rep t
r1 rep t
r2 of
      Just t :~: t
Refl -> forall a. Ord a => a -> a -> Ordering
compare t
t1 t
t2
      Maybe (t :~: t)
Nothing -> forall {k} (t :: k -> *) (a :: k) (b :: k).
Singleton t =>
t a -> t b -> Ordering
cmpIndex rep t
r1 rep t
r2

instance Eq (Shape rep) where
  Shape rep
a == :: Shape rep -> Shape rep -> Bool
== Shape rep
b = forall a. Ord a => a -> a -> Ordering
compare Shape rep
a Shape rep
b forall a. Eq a => a -> a -> Bool
== Ordering
EQ

-- =============================================================
-- Every Singleton type 'r' has Eq(Some r) and Ord(Some r) instances

instance Ord (Some r) where
  compare :: Some r -> Some r -> Ordering
compare (Some r i
x) (Some r i
y) = forall {k} (t :: k -> *) (a :: k) (b :: k).
Singleton t =>
t a -> t b -> Ordering
cmpIndex r i
x r i
y

instance Eq (Some r) where
  (Some r i
x) == :: Some r -> Some r -> Bool
== (Some r i
y) = forall {k} (t :: k -> *) (a :: k) (b :: k).
Singleton t =>
t a -> t b -> Ordering
cmpIndex r i
x r i
y forall a. Eq a => a -> a -> Bool
== Ordering
EQ

-- A strategy for defining Eq and Ord instances for (Any t) if it is Shaped
-- We don't actually make these instances, because there are other strategies
-- we don't want to preclude. But just replace 't' with an indexed type 'R'
-- and supply the (Shaped R TypeRep) instance. Actually any concrete singleton
-- type Rep, can be used in place of TypeRep, as well.
{-
instance Shaped t TypeRep => Eq (Any t) where
  (Any x) == (Any y) = compare @(Shape _) (shape @t @TypeRep x) (shape @t @TypeRep y) == EQ

instance Shaped t TypeRep => Ord (Any t) where
  compare (Any x) (Any y) = compare @(Shape _) (shape @t @TypeRep x) (shape @t @TypeRep y)
-}

-- =======================================================
{- Now we have two ways to make Ord instances for (Some R).
1) if R has a (Singleton R) instance we write

instance Singleton t => Ord (Some t) where
  compare (Some x) (Some y) = cmpIndex @t x y
instance Singleton t => Eq (Some t) where
  x == y = compare x y == EQ

2) if R has a (Shaped R rep) instance we write

instance (forall rep . Shaped t rep) => Ord (Some t) where
  compare (Some x) (Some y) = compare (shape @t x) (shape @t y)
instance (forall rep. Shaped t rep) => Eq (Some t) where
  x == y = compare x y == EQ
-}

-- =============================================================
-- An open Singleton type from Type.Reflection(TypeRep)

compareTypeRep :: TypeRep a -> TypeRep b -> Ordering
compareTypeRep :: forall {k} {k} (a :: k) (b :: k).
TypeRep a -> TypeRep b -> Ordering
compareTypeRep (Con TyCon
x) (Con TyCon
y) = forall a. Ord a => a -> a -> Ordering
compare TyCon
x TyCon
y
compareTypeRep (Con TyCon
_) TypeRep b
_ = Ordering
LT
compareTypeRep TypeRep a
_ (Con TyCon
_) = Ordering
GT
compareTypeRep (App TypeRep a
x TypeRep b
a) (App TypeRep a
y TypeRep b
b) =
  case forall {k} {k} (a :: k) (b :: k).
TypeRep a -> TypeRep b -> Ordering
compareTypeRep TypeRep a
x TypeRep a
y of
    Ordering
EQ -> forall {k} {k} (a :: k) (b :: k).
TypeRep a -> TypeRep b -> Ordering
compareTypeRep TypeRep b
a TypeRep b
b
    Ordering
other -> Ordering
other
#if __GLASGOW_HASKELL__ < 906
-- Ghc-9.6 removed the Fun constructor making these redundant.
compareTypeRep (App TypeRep a
_ TypeRep b
_) TypeRep b
_ = Ordering
LT
compareTypeRep TypeRep a
_ (App TypeRep a
_ TypeRep b
_) = Ordering
GT
compareTypeRep (Fun TypeRep arg
x TypeRep res
a) (Fun TypeRep arg
y TypeRep res
b) =
  case forall {k} {k} (a :: k) (b :: k).
TypeRep a -> TypeRep b -> Ordering
compareTypeRep TypeRep arg
x TypeRep arg
y of
    Ordering
EQ -> forall {k} {k} (a :: k) (b :: k).
TypeRep a -> TypeRep b -> Ordering
compareTypeRep TypeRep res
a TypeRep res
b
    Ordering
other -> Ordering
other
#endif

instance Singleton TypeRep where
  testEql :: forall (i :: k) (j :: k). TypeRep i -> TypeRep j -> Maybe (i :~: j)
testEql = forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality
  cmpIndex :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Ordering
cmpIndex = forall {k} {k} (a :: k) (b :: k).
TypeRep a -> TypeRep b -> Ordering
compareTypeRep

-- =============================================================
-- A very simple closed Singleton type

data R t where
  IntR :: R Int
  BoolR :: R Bool

instance Shaped R any where
  shape :: forall i. R i -> Shape any
shape R i
IntR = forall (rep :: * -> *). Int -> Shape rep
Nullary Int
0
  shape R i
BoolR = forall (rep :: * -> *). Int -> Shape rep
Nullary Int
1

instance Singleton R where
  testEql :: forall i j. R i -> R j -> Maybe (i :~: j)
testEql R i
IntR R j
IntR = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEql R i
BoolR R j
BoolR = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEql R i
_ R j
_ = forall a. Maybe a
Nothing
  cmpIndex :: forall a b. R a -> R b -> Ordering
cmpIndex R a
x R b
y = forall a. Ord a => a -> a -> Ordering
compare @(Shape TypeRep) (forall {k} (t :: k -> *) (rep :: * -> *) (i :: k).
Shaped t rep =>
t i -> Shape rep
shape @R R a
x) (forall {k} (t :: k -> *) (rep :: * -> *) (i :: k).
Shaped t rep =>
t i -> Shape rep
shape @R R b
y)