Foil.hs

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE UndecidableInstances  #-}
-- | This module defines a variation of
-- free scoped (relative) monads relying on the foil for
-- the scope-safe efficient handling of the binders.
--
-- See description of the approach in [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384).
module Control.Monad.Free.Foil where

import           Control.DeepSeq
import qualified Control.Monad.Foil.Internal as Foil
import qualified Control.Monad.Foil.Relative as Foil
import           Data.Bifunctor
import           GHC.Generics                (Generic)

-- | Scoped term under a (single) name binder.
data ScopedAST sig n where
  ScopedAST :: Foil.NameBinder n l -> AST sig l -> ScopedAST sig n

instance (forall l. NFData (AST sig l)) => NFData (ScopedAST sig n) where
  rnf (ScopedAST binder body) = rnf binder `seq` rnf body

-- | A term, generated by a signature 'Bifunctor' @sig@,
-- with (free) variables in scope @n@.
data AST sig n where
  -- | A (free) variable in scope @n@.
  Var :: Foil.Name n -> AST sig n
  -- | A non-variable syntactic construction specified by the signature 'Bifunctor' @sig@.
  Node :: sig (ScopedAST sig n) (AST sig n) -> AST sig n

deriving instance Generic (AST sig n)
deriving instance (forall scope term. (NFData scope, NFData term) => NFData (sig scope term)) => NFData (AST sig n)

instance Bifunctor sig => Foil.Sinkable (AST sig) where
  sinkabilityProof rename = \case
    Var name -> Var (rename name)
    Node node -> Node (bimap f (Foil.sinkabilityProof rename) node)
    where
      f (ScopedAST binder body) =
        Foil.extendRenaming rename binder $ \rename' binder' ->
          ScopedAST binder' (Foil.sinkabilityProof rename' body)

instance Foil.InjectName (AST sig) where
  injectName = Var

-- | Substitution for free (scoped monads).
substitute
  :: (Bifunctor sig, Foil.Distinct o)
  => Foil.Scope o
  -> Foil.Substitution (AST sig) i o
  -> AST sig i
  -> AST sig o
substitute scope subst = \case
  Var name -> Foil.lookupSubst subst name
  Node node -> Node (bimap f (substitute scope subst) node)
  where
    f (ScopedAST binder body) =
      Foil.withRefreshed scope (Foil.nameOf binder) $ \binder' ->
        let subst' = Foil.addRename (Foil.sink subst) binder (Foil.nameOf binder')
            scope' = Foil.extendScope binder' scope
            body' = substitute scope' subst' body
        in ScopedAST binder' body'

-- | @'AST' sig@ is a monad relative to 'Foil.Name'.
instance Bifunctor sig => Foil.RelMonad Foil.Name (AST sig) where
  rreturn = Var
  rbind scope term subst =
    case term of
      Var name  -> subst name
      Node node -> Node (bimap g' g node)
    where
      g x = Foil.rbind scope x subst
      g' (ScopedAST binder body) =
        Foil.withRefreshed scope (Foil.nameOf binder) $ \binder' ->
          let scope' = Foil.extendScope binder' scope
              subst' name = case Foil.unsinkName binder name of
                          Nothing -> Foil.rreturn (Foil.nameOf binder')
                          Just n  -> Foil.sink (subst n)
           in ScopedAST binder' (Foil.rbind scope' body subst')