Algebras.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}


module Control.Monad.IMSOS.Algebras where

import Data.Comp.Multi.Ops ( (:+:)(..))
import Data.Comp.Multi ( Term, Alg, HFunctor (..), (:->) )
import Data.Comp.Multi.Algebra (cata)
import Data.Kind (Type)
import Control.Monad.IMSOS.Signatures (Sort, HasSubSig (SubSig))

class HasAlg f e where
  sem :: Alg f (GetCarrier e)

-- TODO can I get rid of this?
newtype GetCarrier e i = GetCarrier { getCarrier :: CarrierOf e i i }

class HasCarrier e s where
  type CarrierOf e s :: Sort -> Type

instance (HasAlg f e, HasAlg g e)
  => HasAlg (f :+: g) e where
    sem (Inl f) = sem @f f
    sem (Inr g) = sem @g g

eval :: forall eval sig sort.
  (HFunctor sig, HasAlg sig eval)
  => Term sig sort -> GetCarrier eval sort
eval = cata (sem @sig @eval)