{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}

-- |
-- Module      : OAlg.Structure.Definition
-- Description : introducing the idiom of structures
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- introducing the idiom of 'Structure's as parameterized constraints.
module OAlg.Structure.Definition
  (
    -- * Structure
    Structure, Struct(..)

    -- * Transformable
  , Transformable(..), Transformable1(..), TransformableOp
  , ForgetfulTyp

    -- * Some Structure Types
  , Typ, Ord'   

  ) where

import Data.Kind
import Data.Typeable
import Data.Type.Equality

import OAlg.Data.Show
import OAlg.Data.Equal
import OAlg.Data.Ord
import OAlg.Data.Singular
import OAlg.Data.Maybe
import OAlg.Data.Opposite

--------------------------------------------------------------------------------
-- Structure -

-- | parameterized constraint for a type @__x__@.
type family Structure s x :: Constraint

--------------------------------------------------------------------------------
-- Struct -

-- | attest that the type @__x__@ admits the constrains given by the parameter @__s__@.
data Struct s x where
  Struct :: Structure s x => Struct s x

deriving instance Show (Struct s x)
deriving instance Eq (Struct s x)

instance Show1 (Struct s) where
  show1 :: forall x. Struct s x -> String
show1 = forall a. Show a => a -> String
show

instance Eq1 (Struct s) 
instance Singular (Struct s)

--------------------------------------------------------------------------------
-- Typ -

-- | 'Typeable' structures.
data Typ

type instance Structure Typ x = Typeable x

--------------------------------------------------------------------------------
-- Type -

type instance Structure Type x = ()

--------------------------------------------------------------------------------
-- Ord' -

-- | type for ordered structures.
data Ord'

type instance Structure Ord' x = Ord x

--------------------------------------------------------------------------------
-- Transformable -

-- | transforming structural attests.
class Transformable s t where
  tau :: Struct s x -> Struct t x

instance Transformable s s where
  tau :: forall x. Struct s x -> Struct s x
tau Struct s x
s = Struct s x
s

instance Transformable s Type where
  tau :: forall x. Struct s x -> Struct (*) x
tau Struct s x
_ = forall s x. Structure s x => Struct s x
Struct

--------------------------------------------------------------------------------
-- Transformable1 -

-- | transforming structural attests.
class Transformable1 f s where
  tau1 :: Struct s x -> Struct s (f x)

--------------------------------------------------------------------------------
-- TransformableOp -

-- | helper class to avoid undecidable instances.
class Transformable1 Op s => TransformableOp s

--------------------------------------------------------------------------------
-- ForgetfulTyp -

-- | helper class to avoid undecidable instances.
class Transformable s Typ => ForgetfulTyp s


instance Transformable s Typ => TestEquality (Struct s) where
  testEquality :: forall a b. Struct s a -> Struct s b -> Maybe (a :~: b)
testEquality Struct s a
sa Struct s b
sb = forall a b. Struct Typ a -> Struct Typ b -> Maybe (a :~: b)
te (forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct s a
sa) (forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct s b
sb) where
    te :: Struct Typ a -> Struct Typ b -> Maybe (a:~:b)
    te :: forall a b. Struct Typ a -> Struct Typ b -> Maybe (a :~: b)
te Struct Typ a
Struct Struct Typ b
Struct = forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT