LayeredAlgebras.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.LayeredAlgebras where

import Data.Comp.Multi ( HFunctor (..), (:->) )
import Data.Kind (Type)
import Control.Monad.IMSOS.Signatures (Sort, Sig)
import Control.Monad.IMSOS.LayeredTerms (Term (..))
import qualified Data.Comp.Multi as Multi
import Data.Comp.Multi.Ops

type Alg l c = Multi.Alg (Sig l) c

class HasAlg f e where
  sem :: Multi.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

cata :: forall l c. Alg l c -> Term l :-> c
cata f = go 
  where go :: forall j. Term l j -> c j
        go (Term layer) = f (inj (hfmap go layer))

eval :: forall eval l sort. 
  (HasAlg (Sig l) eval)
  => Term l sort -> GetCarrier eval sort 
eval = cata (sem @(Sig l) @eval)