{-# LANGUAGE ConstraintKinds #-} -- For Semantic {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ViewPatterns #-} -- | This module provides the intermediate semantic 'SomeData' -- which interprets combinators as data constructors. -- This enables to pattern-match on combinators -- while keeping their extensibility. module Symantic.Semantics.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 syn. ( Derivable (Data syn sem) , Typeable syn ) => SomeData (Data syn 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 (syn :: Syntax) :: Semantic -> Semantic type instance Derived (Data syn sem) = sem -- | Convenient utility to pattern-match a 'SomeData'. pattern Data :: Typeable syn => Data syn sem a -> SomeData sem a pattern Data x <- (unSomeData -> Maybe.Just x) -- | @(unSomeData sd :: 'Maybe' ('Data' syn sem a))@ -- extract the data-constructor from the given 'SomeData' @(sd)@ -- iif. it belongs to the @('Data' syn sem a)@ data-instance. unSomeData :: forall syn sem a. Typeable syn => SomeData sem a -> Maybe (Data syn sem a) unSomeData (SomeData (constr :: Data actualSyn sem a)) = case typeRep @syn `eqTypeRep` typeRep @actualSyn of Maybe.Just HRefl -> Maybe.Just constr Maybe.Nothing -> Maybe.Nothing -- Abstractable data instance Data Abstractable sem a where Lam :: (SomeData sem a -> SomeData sem b) -> Data Abstractable sem (a -> b) instance (Abstractable sem, Varable sem) => Derivable (Data Abstractable sem) where derive = \case Lam f -> lam (\x -> derive (f (SomeData (Var x)))) instance (Abstractable sem, Varable sem) => Abstractable (SomeData sem) where lam f = SomeData (Lam f) -- Abstractable1 data instance Data Abstractable1 sem a where Lam1 :: (SomeData sem a -> SomeData sem b) -> Data Abstractable1 sem (a -> b) instance (Abstractable1 sem, Varable sem) => Derivable (Data Abstractable1 sem) where derive = \case Lam1 f -> lam1 (\x -> derive (f (SomeData (Var x)))) instance (Abstractable1 sem, Varable sem) => Abstractable1 (SomeData sem) where lam1 f = SomeData (Lam1 f) -- Varable data instance Data Varable sem a where Var :: sem a -> Data Varable sem a instance Varable sem => Derivable (Data Varable sem) where derive = \case Var x -> var x instance Varable sem => Varable (SomeData sem) where 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 => Abstractable1 sem => Instantiable sem => Varable 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 -- Instantiable data instance Data Instantiable sem a where (:@) :: SomeData sem (a -> b) -> SomeData sem a -> Data Instantiable sem b instance Instantiable sem => Derivable (Data Instantiable sem) where derive = \case f :@ x -> derive f .@ derive x instance Instantiable sem => Instantiable (SomeData sem) where f .@ x = SomeData (f :@ x) -- Unabstractable data instance Data Unabstractable sem a where Ap :: Data Unabstractable sem ((a -> b -> c) -> (a -> b) -> a -> c) Const :: Data Unabstractable sem (a -> b -> a) Id :: Data Unabstractable sem (a -> a) (:.) :: Data Unabstractable sem ((b -> c) -> (a -> b) -> a -> c) Flip :: Data Unabstractable sem ((a -> b -> c) -> b -> a -> c) (:$) :: Data Unabstractable sem ((a -> b) -> a -> b) instance Unabstractable sem => Derivable (Data Unabstractable sem) where derive = \case Ap -> ap Const -> const Id -> id (:.) -> (.) Flip -> flip (:$) -> ($) instance Unabstractable sem => Unabstractable (SomeData sem) where ap = SomeData Ap const = SomeData Const id = SomeData Id (.) = SomeData (:.) flip = SomeData Flip ($) = SomeData (:$) -- 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