Data.hs

{-# 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 (SomeData x) = derive 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 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 (SomeData (c :: Data c sem a)) =
  case typeRep @able `eqTypeRep` typeRep @c of
    Maybe.Just HRefl -> Maybe.Just c
    Maybe.Nothing -> 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 = \case
    Lam f -> lam (\x -> derive (f (SomeData (Var x))))
    Lam1 f -> lam1 (\x -> derive (f (SomeData (Var x))))
    Var x -> var x
instance Abstractable sem => Abstractable (SomeData sem) where
  lam f = SomeData (Lam f)
  lam1 f = SomeData (Lam1 f)
  var = 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 = nor
  where
    nor :: SomeData sem b -> SomeData sem b
    nor = \case
      Data (Lam f) -> lam (nor Fun.. f)
      Data (Lam1 f) -> lam1 (nor Fun.. f)
      Data (x :@ y) -> case whnf x of
        Data (Lam1 f) -> nor (f y)
        x' -> nor x' .@ nor y
      Data (IfThenElse test ok ko) ->
        case nor test of
          Data (Constant b :: Data (Constantable Bool) sem Bool) ->
            if b then nor ok else nor ko
          t -> ifThenElse (nor t) (nor ok) (nor ko)
      x -> x

    whnf :: SomeData sem b -> SomeData sem b
    whnf = \case
      Data (x :@ y) -> case whnf x of
        Data (Lam1 f) -> whnf (f y)
        x' -> x' .@ y
      x -> 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 = \case
    f :@ x -> derive f .@ derive x
instance Unabstractable sem => Unabstractable (SomeData sem) where
  f .@ x = SomeData (f :@ x)

-- Functionable
instance
  ( Abstractable sem
  ) =>
  Functionable (SomeData sem)
  where
  ($) = lam1 (\f -> lam1 (\x -> f .@ x))
  (.) = lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
  const = lam1 (\x -> lam1 (\_y -> x))
  flip = lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
  id = lam1 (\x -> 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 = \case
    Anything x -> anything 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 Bottom{} = 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 = \case
    Constant x -> constant x
instance
  ( Constantable c sem
  , Typeable c
  ) =>
  Constantable c (SomeData sem)
  where
  constant c = SomeData (Constant c)
instance{-Typeable c =>-} Constantable c (Data (Constantable c) sem) where
  constant = 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 = \case
    Either -> either
    Left -> left
    Right -> right
instance Eitherable sem => Eitherable (SomeData sem) where
  either = SomeData Either
  left = SomeData Left
  right = SomeData Right
instance Eitherable (Data Eitherable sem) where
  either = Either
  left = Left
  right = 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 = \case
    Equal -> equal
instance
  ( Equalable sem
  ) =>
  Equalable (SomeData sem)
  where
  equal = SomeData Equal
instance Equalable (Data Equalable sem) where
  equal = Equal

-- Emptyable
data instance Data Emptyable sem a where
  Empty :: Data Emptyable sem a
instance Emptyable sem => Derivable (Data Emptyable sem) where
  derive = \case
    Empty -> empty
instance
  ( Emptyable sem
  ) =>
  Emptyable (SomeData sem)
  where
  empty = SomeData Empty
instance Emptyable (Data Emptyable sem) where
  empty = 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 = \case
    Concat -> concat
instance
  ( Semigroupable sem
  ) =>
  Semigroupable (SomeData sem)
  where
  concat = SomeData Concat
instance Semigroupable (Data Semigroupable sem) where
  concat = 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 = \case
    IfThenElse test ok ko -> ifThenElse (derive test) (derive ok) (derive ko)
instance
  ( IfThenElseable sem
  ) =>
  IfThenElseable (SomeData sem)
  where
  ifThenElse test ok ko = SomeData (IfThenElse test ok ko)
instance IfThenElseable sem => IfThenElseable (Data IfThenElseable sem) where
  ifThenElse test ok ko = IfThenElse (SomeData test) (SomeData ok) (SomeData 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 = \case
    Cons -> cons
    Nil -> nil
instance
  ( Listable sem
  ) =>
  Listable (SomeData sem)
  where
  cons = SomeData Cons
  nil = SomeData Nil
instance Listable (Data Listable sem) where
  cons = Cons
  nil = 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 = \case
    Nothing -> nothing
    Just -> just
instance
  ( Maybeable sem
  ) =>
  Maybeable (SomeData sem)
  where
  nothing = SomeData Nothing
  just = SomeData Just
instance Maybeable (Data Maybeable sem) where
  nothing = Nothing
  just = Just