{-# LANGUAGE ConstraintKinds #-}
-- For Semantic
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}

module Symantic.Syntaxes.Data where

import Data.Bool (Bool)
import Data.Either (Either)
import Data.Eq qualified as Eq
import Data.Function qualified as Fun
import Data.Maybe (Maybe)
import Data.Maybe qualified as Maybe
import Data.Semigroup (Semigroup)
import Type.Reflection (Typeable, eqTypeRep, typeRep, (:~~:) (..))

import Symantic.Syntaxes.Classes
import Symantic.Syntaxes.Derive

-- * Type 'SomeData'
data SomeData sem a
  = forall able.
    ( Derivable (Data able sem)
    , Typeable able
    ) =>
    SomeData (Data able sem a)

type instance Derived (SomeData sem) = sem
instance Derivable (SomeData sem) where
  derive :: forall a. SomeData sem a -> Derived (SomeData sem) a
derive (SomeData Data able sem a
x) = Data able sem a -> Derived (Data able sem) a
forall (sem :: * -> *) a. Derivable sem => sem a -> Derived sem a
derive Data able sem a
x

-- ** Type 'Data'

-- TODO: neither data families nor data instances
-- can have phantom roles with GHC-9's RoleAnnotations,
-- hence 'Data.Coerce.coerce' cannot be used on them for now.
-- https://gitlab.haskell.org/ghc/ghc/-/issues/8177
-- https://gitlab.haskell.org/ghc/ghc/-/wikis/roles#proposal-roles-for-type-families
data family Data (able :: Syntax) :: Semantic -> Semantic
type instance Derived (Data able sem) = sem

-- | Convenient utility to pattern-match a 'SomeData'.
pattern Data :: Typeable able => Data able sem a -> SomeData sem a
pattern $mData :: forall {r} {able :: Syntax} {sem :: * -> *} {a}.
Typeable able =>
SomeData sem a -> (Data able sem a -> r) -> (Void# -> r) -> r
Data x <- (unSomeData -> Maybe.Just x)

-- | @(unSomeData c :: 'Maybe' ('Data' able sem a))@
-- extract the data-constructor from the given 'SomeData'
-- iif. it belongs to the @('Data' able sem a)@ data-instance.
unSomeData ::
  forall able sem a.
  Typeable able =>
  SomeData sem a ->
  Maybe (Data able sem a)
unSomeData :: forall (able :: Syntax) (sem :: * -> *) a.
Typeable able =>
SomeData sem a -> Maybe (Data able sem a)
unSomeData (SomeData (Data able sem a
c :: Data c sem a)) =
  case forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: Syntax). Typeable a => TypeRep a
typeRep @able TypeRep able -> TypeRep able -> Maybe (able :~~: able)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`eqTypeRep` forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: Syntax). Typeable a => TypeRep a
typeRep @c of
    Maybe.Just able :~~: able
HRefl -> Data able sem a -> Maybe (Data able sem a)
forall a. a -> Maybe a
Maybe.Just Data able sem a
c
    Maybe (able :~~: able)
Maybe.Nothing -> Maybe (Data able sem a)
forall a. Maybe a
Maybe.Nothing

-- Abstractable
data instance Data Abstractable sem a where
  Lam :: (SomeData sem a -> SomeData sem b) -> Data Abstractable sem (a -> b)
  Lam1 :: (SomeData sem a -> SomeData sem b) -> Data Abstractable sem (a -> b)
  Var :: sem a -> Data Abstractable sem a
instance Abstractable sem => Derivable (Data Abstractable sem) where
  derive :: forall a.
Data Abstractable sem a -> Derived (Data Abstractable sem) a
derive = \case
    Lam SomeData sem a -> SomeData sem b
f -> (sem a -> sem b) -> sem (a -> b)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam (\sem a
x -> SomeData sem b -> Derived (SomeData sem) b
forall (sem :: * -> *) a. Derivable sem => sem a -> Derived sem a
derive (SomeData sem a -> SomeData sem b
f (Data Abstractable sem a -> SomeData sem a
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData (sem a -> Data Abstractable sem a
forall (sem :: * -> *) a. sem a -> Data Abstractable sem a
Var sem a
x))))
    Lam1 SomeData sem a -> SomeData sem b
f -> (sem a -> sem b) -> sem (a -> b)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\sem a
x -> SomeData sem b -> Derived (SomeData sem) b
forall (sem :: * -> *) a. Derivable sem => sem a -> Derived sem a
derive (SomeData sem a -> SomeData sem b
f (Data Abstractable sem a -> SomeData sem a
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData (sem a -> Data Abstractable sem a
forall (sem :: * -> *) a. sem a -> Data Abstractable sem a
Var sem a
x))))
    Var sem a
x -> sem a -> sem a
forall (sem :: * -> *) a. Abstractable sem => sem a -> sem a
var sem a
x
instance Abstractable sem => Abstractable (SomeData sem) where
  lam :: forall a b.
(SomeData sem a -> SomeData sem b) -> SomeData sem (a -> b)
lam SomeData sem a -> SomeData sem b
f = Data Abstractable sem (a -> b) -> SomeData sem (a -> b)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData ((SomeData sem a -> SomeData sem b)
-> Data Abstractable sem (a -> b)
forall (sem :: * -> *) a l.
(SomeData sem a -> SomeData sem l)
-> Data Abstractable sem (a -> l)
Lam SomeData sem a -> SomeData sem b
f)
  lam1 :: forall a b.
(SomeData sem a -> SomeData sem b) -> SomeData sem (a -> b)
lam1 SomeData sem a -> SomeData sem b
f = Data Abstractable sem (a -> b) -> SomeData sem (a -> b)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData ((SomeData sem a -> SomeData sem b)
-> Data Abstractable sem (a -> b)
forall (sem :: * -> *) a l.
(SomeData sem a -> SomeData sem l)
-> Data Abstractable sem (a -> l)
Lam1 SomeData sem a -> SomeData sem b
f)
  var :: forall a. SomeData sem a -> SomeData sem a
var = SomeData sem a -> SomeData sem a
forall a. a -> a
Fun.id

-- | Beta-reduce the left-most outer-most lambda abstraction (aka. normal-order reduction),
-- but to avoid duplication of work, only those manually marked
-- as using their variable at most once.
--
-- DOC: Demonstrating Lambda Calculus Reduction, Peter Sestoft, 2001,
-- https://www.itu.dk/people/sestoft/papers/sestoft-lamreduce.pdf
normalOrderReduction ::
  forall sem a.
  Abstractable sem =>
  IfThenElseable sem =>
  SomeData sem a ->
  SomeData sem a
normalOrderReduction :: forall (sem :: * -> *) a.
(Abstractable sem, IfThenElseable sem) =>
SomeData sem a -> SomeData sem a
normalOrderReduction = SomeData sem a -> SomeData sem a
forall b. SomeData sem b -> SomeData sem b
nor
  where
    nor :: SomeData sem b -> SomeData sem b
    nor :: forall b. SomeData sem b -> SomeData sem b
nor = \case
      Data (Lam SomeData sem a -> SomeData sem b
f) -> (SomeData sem a -> SomeData sem b) -> SomeData sem (a -> b)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam (SomeData sem b -> SomeData sem b
forall b. SomeData sem b -> SomeData sem b
nor (SomeData sem b -> SomeData sem b)
-> (SomeData sem a -> SomeData sem b)
-> SomeData sem a
-> SomeData sem b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. SomeData sem a -> SomeData sem b
f)
      Data (Lam1 SomeData sem a -> SomeData sem b
f) -> (SomeData sem a -> SomeData sem b) -> SomeData sem (a -> b)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (SomeData sem b -> SomeData sem b
forall b. SomeData sem b -> SomeData sem b
nor (SomeData sem b -> SomeData sem b)
-> (SomeData sem a -> SomeData sem b)
-> SomeData sem a
-> SomeData sem b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. SomeData sem a -> SomeData sem b
f)
      Data (SomeData sem (a -> b)
x :@ SomeData sem a
y) -> case SomeData sem (a -> b) -> SomeData sem (a -> b)
forall b. SomeData sem b -> SomeData sem b
whnf SomeData sem (a -> b)
x of
        Data (Lam1 SomeData sem a -> SomeData sem b
f) -> SomeData sem b -> SomeData sem b
forall b. SomeData sem b -> SomeData sem b
nor (SomeData sem a -> SomeData sem b
f SomeData sem a
SomeData sem a
y)
        SomeData sem (a -> b)
x' -> SomeData sem (a -> b) -> SomeData sem (a -> b)
forall b. SomeData sem b -> SomeData sem b
nor SomeData sem (a -> b)
x' SomeData sem (a -> b) -> SomeData sem a -> SomeData sem b
forall (sem :: * -> *) a b.
Unabstractable sem =>
sem (a -> b) -> sem a -> sem b
.@ SomeData sem a -> SomeData sem a
forall b. SomeData sem b -> SomeData sem b
nor SomeData sem a
y
      Data (IfThenElse SomeData sem Bool
test SomeData sem b
ok SomeData sem b
ko) ->
        case SomeData sem Bool -> SomeData sem Bool
forall b. SomeData sem b -> SomeData sem b
nor SomeData sem Bool
test of
          Data (Constant Bool
b :: Data (Constantable Bool) sem Bool) ->
            if Bool
b then SomeData sem b -> SomeData sem b
forall b. SomeData sem b -> SomeData sem b
nor SomeData sem b
ok else SomeData sem b -> SomeData sem b
forall b. SomeData sem b -> SomeData sem b
nor SomeData sem b
ko
          SomeData sem Bool
t -> SomeData sem Bool
-> SomeData sem b -> SomeData sem b -> SomeData sem b
forall (sem :: * -> *) a.
IfThenElseable sem =>
sem Bool -> sem a -> sem a -> sem a
ifThenElse (SomeData sem Bool -> SomeData sem Bool
forall b. SomeData sem b -> SomeData sem b
nor SomeData sem Bool
t) (SomeData sem b -> SomeData sem b
forall b. SomeData sem b -> SomeData sem b
nor SomeData sem b
ok) (SomeData sem b -> SomeData sem b
forall b. SomeData sem b -> SomeData sem b
nor SomeData sem b
ko)
      SomeData sem b
x -> SomeData sem b
x

    whnf :: SomeData sem b -> SomeData sem b
    whnf :: forall b. SomeData sem b -> SomeData sem b
whnf = \case
      Data (SomeData sem (a -> b)
x :@ SomeData sem a
y) -> case SomeData sem (a -> b) -> SomeData sem (a -> b)
forall b. SomeData sem b -> SomeData sem b
whnf SomeData sem (a -> b)
x of
        Data (Lam1 SomeData sem a -> SomeData sem b
f) -> SomeData sem b -> SomeData sem b
forall b. SomeData sem b -> SomeData sem b
whnf (SomeData sem a -> SomeData sem b
f SomeData sem a
SomeData sem a
y)
        SomeData sem (a -> b)
x' -> SomeData sem (a -> b)
x' SomeData sem (a -> b) -> SomeData sem a -> SomeData sem b
forall (sem :: * -> *) a b.
Unabstractable sem =>
sem (a -> b) -> sem a -> sem b
.@ SomeData sem a
y
      SomeData sem b
x -> SomeData sem b
x

-- Unabstractable
data instance Data Unabstractable sem a where
  (:@) :: SomeData sem (a -> b) -> SomeData sem a -> Data Unabstractable sem b
instance Unabstractable sem => Derivable (Data Unabstractable sem) where
  derive :: forall a.
Data Unabstractable sem a -> Derived (Data Unabstractable sem) a
derive = \case
    SomeData sem (a -> a)
f :@ SomeData sem a
x -> SomeData sem (a -> a) -> Derived (SomeData sem) (a -> a)
forall (sem :: * -> *) a. Derivable sem => sem a -> Derived sem a
derive SomeData sem (a -> a)
f sem (a -> a) -> sem a -> sem a
forall (sem :: * -> *) a b.
Unabstractable sem =>
sem (a -> b) -> sem a -> sem b
.@ SomeData sem a -> Derived (SomeData sem) a
forall (sem :: * -> *) a. Derivable sem => sem a -> Derived sem a
derive SomeData sem a
x
instance Unabstractable sem => Unabstractable (SomeData sem) where
  SomeData sem (a -> b)
f .@ :: forall a b.
SomeData sem (a -> b) -> SomeData sem a -> SomeData sem b
.@ SomeData sem a
x = Data Unabstractable sem b -> SomeData sem b
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData (SomeData sem (a -> b)
f SomeData sem (a -> b)
-> SomeData sem a -> Data Unabstractable sem b
forall (sem :: * -> *) a b.
SomeData sem (a -> b)
-> SomeData sem a -> Data Unabstractable sem b
:@ SomeData sem a
x)

-- Functionable
instance
  ( Abstractable sem
  ) =>
  Functionable (SomeData sem)
  where
  $ :: forall a b. SomeData sem ((a -> b) -> a -> b)
($) = (SomeData sem (a -> b) -> SomeData sem (a -> b))
-> SomeData sem ((a -> b) -> a -> b)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem (a -> b)
f -> (SomeData sem a -> SomeData sem b) -> SomeData sem (a -> b)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem a
x -> SomeData sem (a -> b)
f SomeData sem (a -> b) -> SomeData sem a -> SomeData sem b
forall (sem :: * -> *) a b.
Unabstractable sem =>
sem (a -> b) -> sem a -> sem b
.@ SomeData sem a
x))
  . :: forall b c a. SomeData sem ((b -> c) -> (a -> b) -> a -> c)
(.) = (SomeData sem (b -> c) -> SomeData sem ((a -> b) -> a -> c))
-> SomeData sem ((b -> c) -> (a -> b) -> a -> c)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem (b -> c)
f -> (SomeData sem (a -> b) -> SomeData sem (a -> c))
-> SomeData sem ((a -> b) -> a -> c)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem (a -> b)
g -> (SomeData sem a -> SomeData sem c) -> SomeData sem (a -> c)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem a
x -> SomeData sem (b -> c)
f SomeData sem (b -> c) -> SomeData sem b -> SomeData sem c
forall (sem :: * -> *) a b.
Unabstractable sem =>
sem (a -> b) -> sem a -> sem b
.@ (SomeData sem (a -> b)
g SomeData sem (a -> b) -> SomeData sem a -> SomeData sem b
forall (sem :: * -> *) a b.
Unabstractable sem =>
sem (a -> b) -> sem a -> sem b
.@ SomeData sem a
x))))
  const :: forall a b. SomeData sem (a -> b -> a)
const = (SomeData sem a -> SomeData sem (b -> a))
-> SomeData sem (a -> b -> a)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem a
x -> (SomeData sem b -> SomeData sem a) -> SomeData sem (b -> a)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem b
_y -> SomeData sem a
x))
  flip :: forall a b c. SomeData sem ((a -> b -> c) -> b -> a -> c)
flip = (SomeData sem (a -> b -> c) -> SomeData sem (b -> a -> c))
-> SomeData sem ((a -> b -> c) -> b -> a -> c)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem (a -> b -> c)
f -> (SomeData sem b -> SomeData sem (a -> c))
-> SomeData sem (b -> a -> c)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem b
x -> (SomeData sem a -> SomeData sem c) -> SomeData sem (a -> c)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem a
y -> SomeData sem (a -> b -> c)
f SomeData sem (a -> b -> c)
-> SomeData sem a -> SomeData sem (b -> c)
forall (sem :: * -> *) a b.
Unabstractable sem =>
sem (a -> b) -> sem a -> sem b
.@ SomeData sem a
y SomeData sem (b -> c) -> SomeData sem b -> SomeData sem c
forall (sem :: * -> *) a b.
Unabstractable sem =>
sem (a -> b) -> sem a -> sem b
.@ SomeData sem b
x)))
  id :: forall a. SomeData sem (a -> a)
id = (SomeData sem a -> SomeData sem a) -> SomeData sem (a -> a)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem a
x -> SomeData sem a
x)

-- Anythingable
data instance Data Anythingable sem a where
  Anything :: sem a -> Data Anythingable sem a
instance
  ( Anythingable sem
  ) =>
  Derivable (Data Anythingable sem)
  where
  derive :: forall a.
Data Anythingable sem a -> Derived (Data Anythingable sem) a
derive = \case
    Anything sem a
x -> sem a -> sem a
forall (sem :: * -> *) a. Anythingable sem => sem a -> sem a
anything sem a
x
instance Anythingable (SomeData sem)
instance Anythingable (Data Anythingable sem)

-- Bottomable
data instance Data Bottomable sem a where
  Bottom :: Data Bottomable sem a
instance Bottomable sem => Derivable (Data Bottomable sem) where
  derive :: forall a. Data Bottomable sem a -> Derived (Data Bottomable sem) a
derive Bottom{} = Derived (Data Bottomable sem) a
forall (sem :: * -> *) a. Bottomable sem => sem a
bottom

-- Constantable
data instance Data (Constantable c) sem a where
  Constant {-Typeable c =>-} :: c -> Data (Constantable c) sem c
instance Constantable c sem => Derivable (Data (Constantable c) sem) where
  derive :: forall a.
Data (Constantable c) sem a
-> Derived (Data (Constantable c) sem) a
derive = \case
    Constant c
x -> c -> sem c
forall c (sem :: * -> *). Constantable c sem => c -> sem c
constant c
x
instance
  ( Constantable c sem
  , Typeable c
  ) =>
  Constantable c (SomeData sem)
  where
  constant :: c -> SomeData sem c
constant c
c = Data (Constantable c) sem c -> SomeData sem c
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData (c -> Data (Constantable c) sem c
forall c (sem :: * -> *). c -> Data (Constantable c) sem c
Constant c
c)
instance{-Typeable c =>-} Constantable c (Data (Constantable c) sem) where
  constant :: c -> Data (Constantable c) sem c
constant = c -> Data (Constantable c) sem c
forall c (sem :: * -> *). c -> Data (Constantable c) sem c
Constant

-- Eitherable
data instance Data Eitherable sem a where
  Either :: Data Eitherable sem ((l -> a) -> (r -> a) -> Either l r -> a)
  Left :: Data Eitherable sem (l -> Either l r)
  Right :: Data Eitherable sem (r -> Either l r)
instance Eitherable sem => Derivable (Data Eitherable sem) where
  derive :: forall a. Data Eitherable sem a -> Derived (Data Eitherable sem) a
derive = \case
    Data Eitherable sem a
R:DataEitherablesema sem a
Either -> Derived (Data Eitherable sem) a
forall (sem :: * -> *) l a r.
Eitherable sem =>
sem ((l -> a) -> (r -> a) -> Either l r -> a)
either
    Data Eitherable sem a
R:DataEitherablesema sem a
Left -> Derived (Data Eitherable sem) a
forall (sem :: * -> *) l r. Eitherable sem => sem (l -> Either l r)
left
    Data Eitherable sem a
R:DataEitherablesema sem a
Right -> Derived (Data Eitherable sem) a
forall (sem :: * -> *) r l. Eitherable sem => sem (r -> Either l r)
right
instance Eitherable sem => Eitherable (SomeData sem) where
  either :: forall l a r.
SomeData sem ((l -> a) -> (r -> a) -> Either l r -> a)
either = Data Eitherable sem ((l -> a) -> (r -> a) -> Either l r -> a)
-> SomeData sem ((l -> a) -> (r -> a) -> Either l r -> a)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Eitherable sem ((l -> a) -> (r -> a) -> Either l r -> a)
forall (sem :: * -> *) a l r.
Data Eitherable sem ((a -> l) -> (r -> l) -> Either a r -> l)
Either
  left :: forall l r. SomeData sem (l -> Either l r)
left = Data Eitherable sem (l -> Either l r)
-> SomeData sem (l -> Either l r)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Eitherable sem (l -> Either l r)
forall (sem :: * -> *) a l. Data Eitherable sem (a -> Either a l)
Left
  right :: forall r l. SomeData sem (r -> Either l r)
right = Data Eitherable sem (r -> Either l r)
-> SomeData sem (r -> Either l r)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Eitherable sem (r -> Either l r)
forall (sem :: * -> *) a l. Data Eitherable sem (a -> Either l a)
Right
instance Eitherable (Data Eitherable sem) where
  either :: forall l a r.
Data Eitherable sem ((l -> a) -> (r -> a) -> Either l r -> a)
either = Data Eitherable sem ((l -> a) -> (r -> a) -> Either l r -> a)
forall (sem :: * -> *) a l r.
Data Eitherable sem ((a -> l) -> (r -> l) -> Either a r -> l)
Either
  left :: forall l r. Data Eitherable sem (l -> Either l r)
left = Data Eitherable sem (l -> Either l r)
forall (sem :: * -> *) a l. Data Eitherable sem (a -> Either a l)
Left
  right :: forall r l. Data Eitherable sem (r -> Either l r)
right = Data Eitherable sem (r -> Either l r)
forall (sem :: * -> *) a l. Data Eitherable sem (a -> Either l a)
Right

-- Equalable
data instance Data Equalable sem a where
  Equal :: Eq.Eq a => Data Equalable sem (a -> a -> Bool)
instance Equalable sem => Derivable (Data Equalable sem) where
  derive :: forall a. Data Equalable sem a -> Derived (Data Equalable sem) a
derive = \case
    Data Equalable sem a
R:DataEqualablesema sem a
Equal -> Derived (Data Equalable sem) a
forall (sem :: * -> *) a.
(Equalable sem, Eq a) =>
sem (a -> a -> Bool)
equal
instance
  ( Equalable sem
  ) =>
  Equalable (SomeData sem)
  where
  equal :: forall a. Eq a => SomeData sem (a -> a -> Bool)
equal = Data Equalable sem (a -> a -> Bool)
-> SomeData sem (a -> a -> Bool)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Equalable sem (a -> a -> Bool)
forall a (sem :: * -> *).
Eq a =>
Data Equalable sem (a -> a -> Bool)
Equal
instance Equalable (Data Equalable sem) where
  equal :: forall a. Eq a => Data Equalable sem (a -> a -> Bool)
equal = Data Equalable sem (a -> a -> Bool)
forall a (sem :: * -> *).
Eq a =>
Data Equalable sem (a -> a -> Bool)
Equal

-- Emptyable
data instance Data Emptyable sem a where
  Empty :: Data Emptyable sem a
instance Emptyable sem => Derivable (Data Emptyable sem) where
  derive :: forall a. Data Emptyable sem a -> Derived (Data Emptyable sem) a
derive = \case
    Data Emptyable sem a
R:DataEmptyablesema sem a
Empty -> Derived (Data Emptyable sem) a
forall (sem :: * -> *) a. Emptyable sem => sem a
empty
instance
  ( Emptyable sem
  ) =>
  Emptyable (SomeData sem)
  where
  empty :: forall a. SomeData sem a
empty = Data Emptyable sem a -> SomeData sem a
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Emptyable sem a
forall (sem :: * -> *) a. Data Emptyable sem a
Empty
instance Emptyable (Data Emptyable sem) where
  empty :: forall a. Data Emptyable sem a
empty = Data Emptyable sem a
forall (sem :: * -> *) a. Data Emptyable sem a
Empty

-- Semigroupable
data instance Data Semigroupable sem a where
  Concat :: Semigroup a => Data Semigroupable sem (a -> a -> a)
infixr 4 `Concat`
instance Semigroupable sem => Derivable (Data Semigroupable sem) where
  derive :: forall a.
Data Semigroupable sem a -> Derived (Data Semigroupable sem) a
derive = \case
    Data Semigroupable sem a
R:DataSemigroupablesema sem a
Concat -> Derived (Data Semigroupable sem) a
forall (sem :: * -> *) a.
(Semigroupable sem, Semigroup a) =>
sem (a -> a -> a)
concat
instance
  ( Semigroupable sem
  ) =>
  Semigroupable (SomeData sem)
  where
  concat :: forall a. Semigroup a => SomeData sem (a -> a -> a)
concat = Data Semigroupable sem (a -> a -> a) -> SomeData sem (a -> a -> a)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Semigroupable sem (a -> a -> a)
forall a (sem :: * -> *).
Semigroup a =>
Data Semigroupable sem (a -> a -> a)
Concat
instance Semigroupable (Data Semigroupable sem) where
  concat :: forall a. Semigroup a => Data Semigroupable sem (a -> a -> a)
concat = Data Semigroupable sem (a -> a -> a)
forall a (sem :: * -> *).
Semigroup a =>
Data Semigroupable sem (a -> a -> a)
Concat

-- IfThenElseable
data instance Data IfThenElseable sem a where
  IfThenElse ::
    SomeData sem Bool ->
    SomeData sem a ->
    SomeData sem a ->
    Data IfThenElseable sem a
instance IfThenElseable sem => Derivable (Data IfThenElseable sem) where
  derive :: forall a.
Data IfThenElseable sem a -> Derived (Data IfThenElseable sem) a
derive = \case
    IfThenElse SomeData sem Bool
test SomeData sem a
ok SomeData sem a
ko -> sem Bool -> sem a -> sem a -> sem a
forall (sem :: * -> *) a.
IfThenElseable sem =>
sem Bool -> sem a -> sem a -> sem a
ifThenElse (SomeData sem Bool -> Derived (SomeData sem) Bool
forall (sem :: * -> *) a. Derivable sem => sem a -> Derived sem a
derive SomeData sem Bool
test) (SomeData sem a -> Derived (SomeData sem) a
forall (sem :: * -> *) a. Derivable sem => sem a -> Derived sem a
derive SomeData sem a
ok) (SomeData sem a -> Derived (SomeData sem) a
forall (sem :: * -> *) a. Derivable sem => sem a -> Derived sem a
derive SomeData sem a
ko)
instance
  ( IfThenElseable sem
  ) =>
  IfThenElseable (SomeData sem)
  where
  ifThenElse :: forall a.
SomeData sem Bool
-> SomeData sem a -> SomeData sem a -> SomeData sem a
ifThenElse SomeData sem Bool
test SomeData sem a
ok SomeData sem a
ko = Data IfThenElseable sem a -> SomeData sem a
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData (SomeData sem Bool
-> SomeData sem a -> SomeData sem a -> Data IfThenElseable sem a
forall (sem :: * -> *) a.
SomeData sem Bool
-> SomeData sem a -> SomeData sem a -> Data IfThenElseable sem a
IfThenElse SomeData sem Bool
test SomeData sem a
ok SomeData sem a
ko)
instance IfThenElseable sem => IfThenElseable (Data IfThenElseable sem) where
  ifThenElse :: forall a.
Data IfThenElseable sem Bool
-> Data IfThenElseable sem a
-> Data IfThenElseable sem a
-> Data IfThenElseable sem a
ifThenElse Data IfThenElseable sem Bool
test Data IfThenElseable sem a
ok Data IfThenElseable sem a
ko = SomeData sem Bool
-> SomeData sem a -> SomeData sem a -> Data IfThenElseable sem a
forall (sem :: * -> *) a.
SomeData sem Bool
-> SomeData sem a -> SomeData sem a -> Data IfThenElseable sem a
IfThenElse (Data IfThenElseable sem Bool -> SomeData sem Bool
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data IfThenElseable sem Bool
test) (Data IfThenElseable sem a -> SomeData sem a
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data IfThenElseable sem a
ok) (Data IfThenElseable sem a -> SomeData sem a
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data IfThenElseable sem a
ko)

-- Listable
data instance Data Listable sem a where
  Cons :: Data Listable sem (a -> [a] -> [a])
  Nil :: Data Listable sem [a]
infixr 4 `Cons`
instance Listable sem => Derivable (Data Listable sem) where
  derive :: forall a. Data Listable sem a -> Derived (Data Listable sem) a
derive = \case
    Data Listable sem a
R:DataListablesema sem a
Cons -> Derived (Data Listable sem) a
forall (sem :: * -> *) a. Listable sem => sem (a -> [a] -> [a])
cons
    Data Listable sem a
R:DataListablesema sem a
Nil -> Derived (Data Listable sem) a
forall (sem :: * -> *) a. Listable sem => sem [a]
nil
instance
  ( Listable sem
  ) =>
  Listable (SomeData sem)
  where
  cons :: forall a. SomeData sem (a -> [a] -> [a])
cons = Data Listable sem (a -> [a] -> [a])
-> SomeData sem (a -> [a] -> [a])
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Listable sem (a -> [a] -> [a])
forall (sem :: * -> *) a. Data Listable sem (a -> [a] -> [a])
Cons
  nil :: forall a. SomeData sem [a]
nil = Data Listable sem [a] -> SomeData sem [a]
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Listable sem [a]
forall (sem :: * -> *) a. Data Listable sem [a]
Nil
instance Listable (Data Listable sem) where
  cons :: forall a. Data Listable sem (a -> [a] -> [a])
cons = Data Listable sem (a -> [a] -> [a])
forall (sem :: * -> *) a. Data Listable sem (a -> [a] -> [a])
Cons
  nil :: forall a. Data Listable sem [a]
nil = Data Listable sem [a]
forall (sem :: * -> *) a. Data Listable sem [a]
Nil

-- Maybeable
data instance Data Maybeable sem a where
  Nothing :: Data Maybeable sem (Maybe a)
  Just :: Data Maybeable sem (a -> Maybe a)
instance Maybeable sem => Derivable (Data Maybeable sem) where
  derive :: forall a. Data Maybeable sem a -> Derived (Data Maybeable sem) a
derive = \case
    Data Maybeable sem a
R:DataMaybeablesema sem a
Nothing -> Derived (Data Maybeable sem) a
forall (sem :: * -> *) a. Maybeable sem => sem (Maybe a)
nothing
    Data Maybeable sem a
R:DataMaybeablesema sem a
Just -> Derived (Data Maybeable sem) a
forall (sem :: * -> *) a. Maybeable sem => sem (a -> Maybe a)
just
instance
  ( Maybeable sem
  ) =>
  Maybeable (SomeData sem)
  where
  nothing :: forall a. SomeData sem (Maybe a)
nothing = Data Maybeable sem (Maybe a) -> SomeData sem (Maybe a)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Maybeable sem (Maybe a)
forall (sem :: * -> *) a. Data Maybeable sem (Maybe a)
Nothing
  just :: forall a. SomeData sem (a -> Maybe a)
just = Data Maybeable sem (a -> Maybe a) -> SomeData sem (a -> Maybe a)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Maybeable sem (a -> Maybe a)
forall (sem :: * -> *) a. Data Maybeable sem (a -> Maybe a)
Just
instance Maybeable (Data Maybeable sem) where
  nothing :: forall a. Data Maybeable sem (Maybe a)
nothing = Data Maybeable sem (Maybe a)
forall (sem :: * -> *) a. Data Maybeable sem (Maybe a)
Nothing
  just :: forall a. Data Maybeable sem (a -> Maybe a)
just = Data Maybeable sem (a -> Maybe a)
forall (sem :: * -> *) a. Data Maybeable sem (a -> Maybe a)
Just