{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DerivingStrategies #-}
{-# language DeriveAnyClass #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# language CPP #-}
{-# options_ghc -Wno-unused-top-binds #-}
-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2013 Edward Kmett
--                (C) 2021 Marco Zocca (ocramz)
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  ocramz
-- Stability   :  experimental
-- Portability :  portable
--
-- 'Scope' is to be used inside of the definition of binders.
--
-- A lightweight implementation of 'bound'. Provides much of the functionality of Bound.Scope.Simple, without the large dependency footprint.
--
-- = Example
--
-- The 'whnf' function in this example shows how to beta-reduce a term of the untyped lambda calculus.
--
-- Note : the Show instance of Exp depends on its Show1 instance (since Exp has one type parameter), which can be derived 'Generically' thanks to DerivingVia. This works on most recent versions of GHC (>= 8.6.1).
--
-- @
-- {-# LANGUAGE DeriveFunctor #-}
-- {-# LANGUAGE DeriveFoldable #-}
-- {-# LANGUAGE DeriveTraversable #-}
--
-- import Bound.Simple (Scope, Bound(..), abstract1, instantiate1)
-- import Data.Functor.Classes.Generic (Generically(..))
-- 
-- import GHC.Generics (Generic1)
--
-- infixl 9 :\@
-- data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
--   deriving (Show, Functor, Foldable, Traversable, Generic1)
--   deriving (Show1) via Generically Exp
--
-- instance Applicative Exp where pure = V; k \<*\> m = ap k m
--
-- instance Monad Exp where
--   return = V
--   V a      >>= f = f a
--   (x :\@ y) >>= f = (x >>= f) :\@ (y >>= f)
--   Lam e    >>= f = Lam (e '>>>=' f)
--
-- lam :: Eq a => a -> Exp a -> Exp a
-- lam v b = Lam ('abstract1' v b)
--
-- whnf :: Exp a -> Exp a
-- whnf (e1 \:\@ e2) = case whnf e1 of
--   Lam b -> whnf ('instantiate1' e2 b)
--   f'    -> f' :\@ e2
-- whnf e = e
--
-- main :: IO ()
-- main = do
--   let term = lam 'x' (V 'x') :\@ V 'y'
--   print term         -- Lam (Scope (V (B ()))) :\@ V 'y'
--   print $ whnf term  -- V 'y'
-- @
----------------------------------------------------------------------------


module Bound.Simple (Bound(..)
                    , Scope, toScope, fromScope
                    , Var
                    -- * Abstraction
                    , abstract, abstract1
                    -- * Instantiation
                    , instantiate, instantiate1
                    , bindings
                    , hoistScope
                    , closed
                    , substitute
                    , substituteVar
                    -- ** Predicates
                    , isClosed
                    -- * Utils
                    , Generically(..)
                    ) where

import Control.Monad (ap, liftM)
import Control.Monad.Trans.Class (MonadTrans(..))
import Data.Functor.Classes (Show2(..), Show1(..), showsUnaryWith, showsPrec1, liftShowsPrec2, Eq2(..), Eq1(..), eq1, liftEq, liftEq2)
import GHC.Generics (Generic1)
import Data.Functor.Classes.Generic (Generically(..))

infixl 9 :@
data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
  deriving (Int -> Exp a -> ShowS
[Exp a] -> ShowS
Exp a -> String
(Int -> Exp a -> ShowS)
-> (Exp a -> String) -> ([Exp a] -> ShowS) -> Show (Exp a)
forall a. Show a => Int -> Exp a -> ShowS
forall a. Show a => [Exp a] -> ShowS
forall a. Show a => Exp a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Exp a] -> ShowS
$cshowList :: forall a. Show a => [Exp a] -> ShowS
show :: Exp a -> String
$cshow :: forall a. Show a => Exp a -> String
showsPrec :: Int -> Exp a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Exp a -> ShowS
Show, Exp a -> Exp a -> Bool
(Exp a -> Exp a -> Bool) -> (Exp a -> Exp a -> Bool) -> Eq (Exp a)
forall a. Eq a => Exp a -> Exp a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Exp a -> Exp a -> Bool
$c/= :: forall a. Eq a => Exp a -> Exp a -> Bool
== :: Exp a -> Exp a -> Bool
$c== :: forall a. Eq a => Exp a -> Exp a -> Bool
Eq, a -> Exp b -> Exp a
(a -> b) -> Exp a -> Exp b
(forall a b. (a -> b) -> Exp a -> Exp b)
-> (forall a b. a -> Exp b -> Exp a) -> Functor Exp
forall a b. a -> Exp b -> Exp a
forall a b. (a -> b) -> Exp a -> Exp b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Exp b -> Exp a
$c<$ :: forall a b. a -> Exp b -> Exp a
fmap :: (a -> b) -> Exp a -> Exp b
$cfmap :: forall a b. (a -> b) -> Exp a -> Exp b
Functor,Exp a -> Bool
(a -> m) -> Exp a -> m
(a -> b -> b) -> b -> Exp a -> b
(forall m. Monoid m => Exp m -> m)
-> (forall m a. Monoid m => (a -> m) -> Exp a -> m)
-> (forall m a. Monoid m => (a -> m) -> Exp a -> m)
-> (forall a b. (a -> b -> b) -> b -> Exp a -> b)
-> (forall a b. (a -> b -> b) -> b -> Exp a -> b)
-> (forall b a. (b -> a -> b) -> b -> Exp a -> b)
-> (forall b a. (b -> a -> b) -> b -> Exp a -> b)
-> (forall a. (a -> a -> a) -> Exp a -> a)
-> (forall a. (a -> a -> a) -> Exp a -> a)
-> (forall a. Exp a -> [a])
-> (forall a. Exp a -> Bool)
-> (forall a. Exp a -> Int)
-> (forall a. Eq a => a -> Exp a -> Bool)
-> (forall a. Ord a => Exp a -> a)
-> (forall a. Ord a => Exp a -> a)
-> (forall a. Num a => Exp a -> a)
-> (forall a. Num a => Exp a -> a)
-> Foldable Exp
forall a. Eq a => a -> Exp a -> Bool
forall a. Num a => Exp a -> a
forall a. Ord a => Exp a -> a
forall m. Monoid m => Exp m -> m
forall a. Exp a -> Bool
forall a. Exp a -> Int
forall a. Exp a -> [a]
forall a. (a -> a -> a) -> Exp a -> a
forall m a. Monoid m => (a -> m) -> Exp a -> m
forall b a. (b -> a -> b) -> b -> Exp a -> b
forall a b. (a -> b -> b) -> b -> Exp a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Exp a -> a
$cproduct :: forall a. Num a => Exp a -> a
sum :: Exp a -> a
$csum :: forall a. Num a => Exp a -> a
minimum :: Exp a -> a
$cminimum :: forall a. Ord a => Exp a -> a
maximum :: Exp a -> a
$cmaximum :: forall a. Ord a => Exp a -> a
elem :: a -> Exp a -> Bool
$celem :: forall a. Eq a => a -> Exp a -> Bool
length :: Exp a -> Int
$clength :: forall a. Exp a -> Int
null :: Exp a -> Bool
$cnull :: forall a. Exp a -> Bool
toList :: Exp a -> [a]
$ctoList :: forall a. Exp a -> [a]
foldl1 :: (a -> a -> a) -> Exp a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Exp a -> a
foldr1 :: (a -> a -> a) -> Exp a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Exp a -> a
foldl' :: (b -> a -> b) -> b -> Exp a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Exp a -> b
foldl :: (b -> a -> b) -> b -> Exp a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Exp a -> b
foldr' :: (a -> b -> b) -> b -> Exp a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Exp a -> b
foldr :: (a -> b -> b) -> b -> Exp a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Exp a -> b
foldMap' :: (a -> m) -> Exp a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Exp a -> m
foldMap :: (a -> m) -> Exp a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Exp a -> m
fold :: Exp m -> m
$cfold :: forall m. Monoid m => Exp m -> m
Foldable,Functor Exp
Foldable Exp
Functor Exp
-> Foldable Exp
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Exp a -> f (Exp b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Exp (f a) -> f (Exp a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Exp a -> m (Exp b))
-> (forall (m :: * -> *) a. Monad m => Exp (m a) -> m (Exp a))
-> Traversable Exp
(a -> f b) -> Exp a -> f (Exp b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Exp (m a) -> m (Exp a)
forall (f :: * -> *) a. Applicative f => Exp (f a) -> f (Exp a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Exp a -> m (Exp b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Exp a -> f (Exp b)
sequence :: Exp (m a) -> m (Exp a)
$csequence :: forall (m :: * -> *) a. Monad m => Exp (m a) -> m (Exp a)
mapM :: (a -> m b) -> Exp a -> m (Exp b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Exp a -> m (Exp b)
sequenceA :: Exp (f a) -> f (Exp a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Exp (f a) -> f (Exp a)
traverse :: (a -> f b) -> Exp a -> f (Exp b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Exp a -> f (Exp b)
$cp2Traversable :: Foldable Exp
$cp1Traversable :: Functor Exp
Traversable, (forall a. Exp a -> Rep1 Exp a)
-> (forall a. Rep1 Exp a -> Exp a) -> Generic1 Exp
forall a. Rep1 Exp a -> Exp a
forall a. Exp a -> Rep1 Exp a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cto1 :: forall a. Rep1 Exp a -> Exp a
$cfrom1 :: forall a. Exp a -> Rep1 Exp a
Generic1)
  deriving ((Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Exp a -> ShowS
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [Exp a] -> ShowS
(forall a.
 (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Exp a -> ShowS)
-> (forall a.
    (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Exp a] -> ShowS)
-> Show1 Exp
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Exp a -> ShowS
forall a. (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Exp a] -> ShowS
forall (f :: * -> *).
(forall a.
 (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS)
-> (forall a.
    (Int -> a -> ShowS) -> ([a] -> ShowS) -> [f a] -> ShowS)
-> Show1 f
liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Exp a] -> ShowS
$cliftShowList :: forall a. (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Exp a] -> ShowS
liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Exp a -> ShowS
$cliftShowsPrec :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Exp a -> ShowS
Show1, (a -> b -> Bool) -> Exp a -> Exp b -> Bool
(forall a b. (a -> b -> Bool) -> Exp a -> Exp b -> Bool) -> Eq1 Exp
forall a b. (a -> b -> Bool) -> Exp a -> Exp b -> Bool
forall (f :: * -> *).
(forall a b. (a -> b -> Bool) -> f a -> f b -> Bool) -> Eq1 f
liftEq :: (a -> b -> Bool) -> Exp a -> Exp b -> Bool
$cliftEq :: forall a b. (a -> b -> Bool) -> Exp a -> Exp b -> Bool
Eq1) via Generically Exp

-- instance Applicative Exp where pure = V; (<*>) = ap

-- instance Monad Exp where
--   return = V
--   V a      >>= f = f a
--   (x :@ y) >>= f = (x >>= f) :@ (y >>= f)
--   Lam e    >>= f = Lam (e >>>= f)

-- lam :: Eq a => a -> Exp a -> Exp a
-- lam v b = Lam (abstract1 v b)

-- whnf :: Exp a -> Exp a
-- whnf (f :@ a) = case whnf f of
--   Lam b -> whnf (instantiate1 a b)
--   f'    -> f' :@ a
-- whnf e = e

-- test :: IO ()
-- test = do
--   let term = lam 'x' (V 'x') :@ V 'y'
--   print $ term
--   print $ whnf term


data Var b a = B b -- ^ bound variables
             | F a -- ^ free variables
             deriving (Var b a -> Var b a -> Bool
(Var b a -> Var b a -> Bool)
-> (Var b a -> Var b a -> Bool) -> Eq (Var b a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall b a. (Eq b, Eq a) => Var b a -> Var b a -> Bool
/= :: Var b a -> Var b a -> Bool
$c/= :: forall b a. (Eq b, Eq a) => Var b a -> Var b a -> Bool
== :: Var b a -> Var b a -> Bool
$c== :: forall b a. (Eq b, Eq a) => Var b a -> Var b a -> Bool
Eq, Int -> Var b a -> ShowS
[Var b a] -> ShowS
Var b a -> String
(Int -> Var b a -> ShowS)
-> (Var b a -> String) -> ([Var b a] -> ShowS) -> Show (Var b a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall b a. (Show b, Show a) => Int -> Var b a -> ShowS
forall b a. (Show b, Show a) => [Var b a] -> ShowS
forall b a. (Show b, Show a) => Var b a -> String
showList :: [Var b a] -> ShowS
$cshowList :: forall b a. (Show b, Show a) => [Var b a] -> ShowS
show :: Var b a -> String
$cshow :: forall b a. (Show b, Show a) => Var b a -> String
showsPrec :: Int -> Var b a -> ShowS
$cshowsPrec :: forall b a. (Show b, Show a) => Int -> Var b a -> ShowS
Show, a -> Var b b -> Var b a
(a -> b) -> Var b a -> Var b b
(forall a b. (a -> b) -> Var b a -> Var b b)
-> (forall a b. a -> Var b b -> Var b a) -> Functor (Var b)
forall a b. a -> Var b b -> Var b a
forall a b. (a -> b) -> Var b a -> Var b b
forall b a b. a -> Var b b -> Var b a
forall b a b. (a -> b) -> Var b a -> Var b b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Var b b -> Var b a
$c<$ :: forall b a b. a -> Var b b -> Var b a
fmap :: (a -> b) -> Var b a -> Var b b
$cfmap :: forall b a b. (a -> b) -> Var b a -> Var b b
Functor, Var b a -> Bool
(a -> m) -> Var b a -> m
(a -> b -> b) -> b -> Var b a -> b
(forall m. Monoid m => Var b m -> m)
-> (forall m a. Monoid m => (a -> m) -> Var b a -> m)
-> (forall m a. Monoid m => (a -> m) -> Var b a -> m)
-> (forall a b. (a -> b -> b) -> b -> Var b a -> b)
-> (forall a b. (a -> b -> b) -> b -> Var b a -> b)
-> (forall b a. (b -> a -> b) -> b -> Var b a -> b)
-> (forall b a. (b -> a -> b) -> b -> Var b a -> b)
-> (forall a. (a -> a -> a) -> Var b a -> a)
-> (forall a. (a -> a -> a) -> Var b a -> a)
-> (forall a. Var b a -> [a])
-> (forall a. Var b a -> Bool)
-> (forall a. Var b a -> Int)
-> (forall a. Eq a => a -> Var b a -> Bool)
-> (forall a. Ord a => Var b a -> a)
-> (forall a. Ord a => Var b a -> a)
-> (forall a. Num a => Var b a -> a)
-> (forall a. Num a => Var b a -> a)
-> Foldable (Var b)
forall a. Eq a => a -> Var b a -> Bool
forall a. Num a => Var b a -> a
forall a. Ord a => Var b a -> a
forall m. Monoid m => Var b m -> m
forall a. Var b a -> Bool
forall a. Var b a -> Int
forall a. Var b a -> [a]
forall a. (a -> a -> a) -> Var b a -> a
forall b a. Eq a => a -> Var b a -> Bool
forall b a. Num a => Var b a -> a
forall b a. Ord a => Var b a -> a
forall m a. Monoid m => (a -> m) -> Var b a -> m
forall b m. Monoid m => Var b m -> m
forall b a. Var b a -> Bool
forall b a. Var b a -> Int
forall b a. Var b a -> [a]
forall b a. (b -> a -> b) -> b -> Var b a -> b
forall a b. (a -> b -> b) -> b -> Var b a -> b
forall b a. (a -> a -> a) -> Var b a -> a
forall b m a. Monoid m => (a -> m) -> Var b a -> m
forall b b a. (b -> a -> b) -> b -> Var b a -> b
forall b a b. (a -> b -> b) -> b -> Var b a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Var b a -> a
$cproduct :: forall b a. Num a => Var b a -> a
sum :: Var b a -> a
$csum :: forall b a. Num a => Var b a -> a
minimum :: Var b a -> a
$cminimum :: forall b a. Ord a => Var b a -> a
maximum :: Var b a -> a
$cmaximum :: forall b a. Ord a => Var b a -> a
elem :: a -> Var b a -> Bool
$celem :: forall b a. Eq a => a -> Var b a -> Bool
length :: Var b a -> Int
$clength :: forall b a. Var b a -> Int
null :: Var b a -> Bool
$cnull :: forall b a. Var b a -> Bool
toList :: Var b a -> [a]
$ctoList :: forall b a. Var b a -> [a]
foldl1 :: (a -> a -> a) -> Var b a -> a
$cfoldl1 :: forall b a. (a -> a -> a) -> Var b a -> a
foldr1 :: (a -> a -> a) -> Var b a -> a
$cfoldr1 :: forall b a. (a -> a -> a) -> Var b a -> a
foldl' :: (b -> a -> b) -> b -> Var b a -> b
$cfoldl' :: forall b b a. (b -> a -> b) -> b -> Var b a -> b
foldl :: (b -> a -> b) -> b -> Var b a -> b
$cfoldl :: forall b b a. (b -> a -> b) -> b -> Var b a -> b
foldr' :: (a -> b -> b) -> b -> Var b a -> b
$cfoldr' :: forall b a b. (a -> b -> b) -> b -> Var b a -> b
foldr :: (a -> b -> b) -> b -> Var b a -> b
$cfoldr :: forall b a b. (a -> b -> b) -> b -> Var b a -> b
foldMap' :: (a -> m) -> Var b a -> m
$cfoldMap' :: forall b m a. Monoid m => (a -> m) -> Var b a -> m
foldMap :: (a -> m) -> Var b a -> m
$cfoldMap :: forall b m a. Monoid m => (a -> m) -> Var b a -> m
fold :: Var b m -> m
$cfold :: forall b m. Monoid m => Var b m -> m
Foldable, Functor (Var b)
Foldable (Var b)
Functor (Var b)
-> Foldable (Var b)
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Var b a -> f (Var b b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Var b (f a) -> f (Var b a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Var b a -> m (Var b b))
-> (forall (m :: * -> *) a. Monad m => Var b (m a) -> m (Var b a))
-> Traversable (Var b)
(a -> f b) -> Var b a -> f (Var b b)
forall b. Functor (Var b)
forall b. Foldable (Var b)
forall b (m :: * -> *) a. Monad m => Var b (m a) -> m (Var b a)
forall b (f :: * -> *) a.
Applicative f =>
Var b (f a) -> f (Var b a)
forall b (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Var b a -> m (Var b b)
forall b (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Var b a -> f (Var b b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Var b (m a) -> m (Var b a)
forall (f :: * -> *) a. Applicative f => Var b (f a) -> f (Var b a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Var b a -> m (Var b b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Var b a -> f (Var b b)
sequence :: Var b (m a) -> m (Var b a)
$csequence :: forall b (m :: * -> *) a. Monad m => Var b (m a) -> m (Var b a)
mapM :: (a -> m b) -> Var b a -> m (Var b b)
$cmapM :: forall b (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Var b a -> m (Var b b)
sequenceA :: Var b (f a) -> f (Var b a)
$csequenceA :: forall b (f :: * -> *) a.
Applicative f =>
Var b (f a) -> f (Var b a)
traverse :: (a -> f b) -> Var b a -> f (Var b b)
$ctraverse :: forall b (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Var b a -> f (Var b b)
$cp2Traversable :: forall b. Foldable (Var b)
$cp1Traversable :: forall b. Functor (Var b)
Traversable)
instance Eq2 Var where
  liftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> Var a c -> Var b d -> Bool
liftEq2 a -> b -> Bool
f c -> d -> Bool
_ (B a
a) (B b
c) = a -> b -> Bool
f a
a b
c
  liftEq2 a -> b -> Bool
_ c -> d -> Bool
g (F c
b) (F d
d) = c -> d -> Bool
g c
b d
d
  liftEq2 a -> b -> Bool
_ c -> d -> Bool
_ Var a c
_ Var b d
_ = Bool
False
instance Eq b => Eq1 (Var b) where liftEq :: (a -> b -> Bool) -> Var b a -> Var b b -> Bool
liftEq = (b -> b -> Bool) -> (a -> b -> Bool) -> Var b a -> Var b b -> Bool
forall (f :: * -> * -> *) a b c d.
Eq2 f =>
(a -> b -> Bool) -> (c -> d -> Bool) -> f a c -> f b d -> Bool
liftEq2 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
(==)
instance Show2 Var where
  liftShowsPrec2 :: (Int -> a -> ShowS)
-> ([a] -> ShowS)
-> (Int -> b -> ShowS)
-> ([b] -> ShowS)
-> Int
-> Var a b
-> ShowS
liftShowsPrec2 Int -> a -> ShowS
f [a] -> ShowS
_ Int -> b -> ShowS
_ [b] -> ShowS
_ Int
d (B a
a) = (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith Int -> a -> ShowS
f String
"B" Int
d a
a
  liftShowsPrec2 Int -> a -> ShowS
_ [a] -> ShowS
_ Int -> b -> ShowS
h [b] -> ShowS
_ Int
d (F b
a) = (Int -> b -> ShowS) -> String -> Int -> b -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith Int -> b -> ShowS
h String
"F" Int
d b
a
instance Show b => Show1 (Var b) where
  liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Var b a -> ShowS
liftShowsPrec = (Int -> b -> ShowS)
-> ([b] -> ShowS)
-> (Int -> a -> ShowS)
-> ([a] -> ShowS)
-> Int
-> Var b a
-> ShowS
forall (f :: * -> * -> *) a b.
Show2 f =>
(Int -> a -> ShowS)
-> ([a] -> ShowS)
-> (Int -> b -> ShowS)
-> ([b] -> ShowS)
-> Int
-> f a b
-> ShowS
liftShowsPrec2 Int -> b -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec [b] -> ShowS
forall a. Show a => [a] -> ShowS
showList

-- | @'Scope' b f a@ is an @f@ expression with bound variables in @b@,
-- and free variables in @a@
newtype Scope b f a = Scope { Scope b f a -> f (Var b a)
unscope :: f (Var b a) }
  deriving ((forall a. Scope b f a -> Rep1 (Scope b f) a)
-> (forall a. Rep1 (Scope b f) a -> Scope b f a)
-> Generic1 (Scope b f)
forall a. Rep1 (Scope b f) a -> Scope b f a
forall a. Scope b f a -> Rep1 (Scope b f) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
forall b (f :: * -> *) a.
Functor f =>
Rep1 (Scope b f) a -> Scope b f a
forall b (f :: * -> *) a.
Functor f =>
Scope b f a -> Rep1 (Scope b f) a
$cto1 :: forall b (f :: * -> *) a.
Functor f =>
Rep1 (Scope b f) a -> Scope b f a
$cfrom1 :: forall b (f :: * -> *) a.
Functor f =>
Scope b f a -> Rep1 (Scope b f) a
Generic1)
  deriving ((Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> Scope b f a -> ShowS
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [Scope b f a] -> ShowS
(forall a.
 (Int -> a -> ShowS)
 -> ([a] -> ShowS) -> Int -> Scope b f a -> ShowS)
-> (forall a.
    (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Scope b f a] -> ShowS)
-> Show1 (Scope b f)
forall a.
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> Scope b f a -> ShowS
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [Scope b f a] -> ShowS
forall b (f :: * -> *) a.
(Functor f, Show1 f, Show b) =>
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> Scope b f a -> ShowS
forall b (f :: * -> *) a.
(Functor f, Show1 f, Show b) =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [Scope b f a] -> ShowS
forall (f :: * -> *).
(forall a.
 (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS)
-> (forall a.
    (Int -> a -> ShowS) -> ([a] -> ShowS) -> [f a] -> ShowS)
-> Show1 f
liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Scope b f a] -> ShowS
$cliftShowList :: forall b (f :: * -> *) a.
(Functor f, Show1 f, Show b) =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [Scope b f a] -> ShowS
liftShowsPrec :: (Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> Scope b f a -> ShowS
$cliftShowsPrec :: forall b (f :: * -> *) a.
(Functor f, Show1 f, Show b) =>
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> Scope b f a -> ShowS
Show1, (a -> b -> Bool) -> Scope b f a -> Scope b f b -> Bool
(forall a b.
 (a -> b -> Bool) -> Scope b f a -> Scope b f b -> Bool)
-> Eq1 (Scope b f)
forall a b. (a -> b -> Bool) -> Scope b f a -> Scope b f b -> Bool
forall b (f :: * -> *) a b.
(Functor f, Eq1 f, Eq b) =>
(a -> b -> Bool) -> Scope b f a -> Scope b f b -> Bool
forall (f :: * -> *).
(forall a b. (a -> b -> Bool) -> f a -> f b -> Bool) -> Eq1 f
liftEq :: (a -> b -> Bool) -> Scope b f a -> Scope b f b -> Bool
$cliftEq :: forall b (f :: * -> *) a b.
(Functor f, Eq1 f, Eq b) =>
(a -> b -> Bool) -> Scope b f a -> Scope b f b -> Bool
Eq1) via (Generically (Scope b f))

-- instance (Eq b, Eq1 f) => Eq1 (Scope b f)  where
--   liftEq f m n = liftEq (liftEq f) (unscope m) (unscope n)
-- instance (Show b, Show1 f) => Show1 (Scope b f) where
--   liftShowsPrec f g d m = showParen (d > 10) $
--     showString "Scope " . liftShowsPrec (liftShowsPrec f g) (liftShowList f g) 11 (unscope m)
instance (Eq e, Functor m, Eq1 m, Eq a) => Eq (Scope e m a) where == :: Scope e m a -> Scope e m a -> Bool
(==) = Scope e m a -> Scope e m a -> Bool
forall (f :: * -> *) a. (Eq1 f, Eq a) => f a -> f a -> Bool
eq1
instance (Show e, Functor m, Show1 m, Show a) => Show (Scope e m a) where showsPrec :: Int -> Scope e m a -> ShowS
showsPrec = Int -> Scope e m a -> ShowS
forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1

-- | @'fromScope'@ is just another name for 'unscope'
fromScope :: Scope b f a -> f (Var b a)
fromScope :: Scope b f a -> f (Var b a)
fromScope = Scope b f a -> f (Var b a)
forall b (f :: * -> *) a. Scope b f a -> f (Var b a)
unscope
{-# INLINE fromScope #-}

-- | @'toScope'@ is just another name for 'Scope'
toScope :: f (Var b a) -> Scope b f a
toScope :: f (Var b a) -> Scope b f a
toScope = f (Var b a) -> Scope b f a
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope
{-# INLINE toScope #-}

class Bound t where
  -- | Perform substitution
  --
  -- If @t@ is an instance of @MonadTrans@ and you are compiling on GHC >= 7.4, then this
  -- gets the default definition:
  --
  -- @m '>>>=' f = m '>>=' 'lift' '.' f@
  (>>>=) :: Monad f => t f a -> (a -> f c) -> t f c
#if defined(__GLASGOW_HASKELL__)
  default (>>>=) :: (MonadTrans t, Monad f, Monad (t f)) =>
                    t f a -> (a -> f c) -> t f c
  t f a
m >>>= a -> f c
f = t f a
m t f a -> (a -> t f c) -> t f c
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= f c -> t f c
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (f c -> t f c) -> (a -> f c) -> a -> t f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f c
f
  {-# INLINE (>>>=) #-}
#endif

instance Bound (Scope b) where
  Scope f (Var b a)
m >>>= :: Scope b f a -> (a -> f c) -> Scope b f c
>>>= a -> f c
f = f (Var b c) -> Scope b f c
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope (f (Var b c) -> Scope b f c) -> f (Var b c) -> Scope b f c
forall a b. (a -> b) -> a -> b
$ f (Var b a)
m f (Var b a) -> (Var b a -> f (Var b c)) -> f (Var b c)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Var b a
v -> case Var b a
v of
    B b
b -> Var b c -> f (Var b c)
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> Var b c
forall b a. b -> Var b a
B b
b)
    F a
a -> (c -> Var b c) -> f c -> f (Var b c)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM c -> Var b c
forall b a. a -> Var b a
F (a -> f c
f a
a)
  {-# INLINE (>>>=) #-}

instance Functor f => Functor (Scope b f) where
  fmap :: (a -> b) -> Scope b f a -> Scope b f b
fmap a -> b
f (Scope f (Var b a)
a) = f (Var b b) -> Scope b f b
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope ((Var b a -> Var b b) -> f (Var b a) -> f (Var b b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> Var b a -> Var b b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) f (Var b a)
a)
  {-# INLINE fmap #-}

-- | @'toList'@ is provides a list (with duplicates) of the free variables
instance Foldable f => Foldable (Scope b f) where
  foldMap :: (a -> m) -> Scope b f a -> m
foldMap a -> m
f (Scope f (Var b a)
a) = (Var b a -> m) -> f (Var b a) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((a -> m) -> Var b a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f) f (Var b a)
a
  {-# INLINE foldMap #-}

instance Traversable f => Traversable (Scope b f) where
  traverse :: (a -> f b) -> Scope b f a -> f (Scope b f b)
traverse a -> f b
f (Scope f (Var b a)
a) = f (Var b b) -> Scope b f b
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope (f (Var b b) -> Scope b f b) -> f (f (Var b b)) -> f (Scope b f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var b a -> f (Var b b)) -> f (Var b a) -> f (f (Var b b))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> f b) -> Var b a -> f (Var b b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f) f (Var b a)
a
  {-# INLINE traverse #-}

#if !MIN_VERSION_base(4,8,0)
instance (Functor f, Monad f) => Applicative (Scope b f) where
#else
instance Monad f => Applicative (Scope b f) where
#endif
  pure :: a -> Scope b f a
pure a
a = f (Var b a) -> Scope b f a
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope (Var b a -> f (Var b a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Var b a
forall b a. a -> Var b a
F a
a))
  {-# INLINE pure #-}
  <*> :: Scope b f (a -> b) -> Scope b f a -> Scope b f b
(<*>) = Scope b f (a -> b) -> Scope b f a -> Scope b f b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
  {-# INLINE (<*>) #-}

-- | The monad permits substitution on free variables, while preserving
-- bound variables
instance Monad f => Monad (Scope b f) where
#if __GLASGOW_HASKELL__ < 710
  return a = Scope (return (F a))
  {-# INLINE return #-}
#endif
  Scope f (Var b a)
e >>= :: Scope b f a -> (a -> Scope b f b) -> Scope b f b
>>= a -> Scope b f b
f = f (Var b b) -> Scope b f b
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope (f (Var b b) -> Scope b f b) -> f (Var b b) -> Scope b f b
forall a b. (a -> b) -> a -> b
$ f (Var b a)
e f (Var b a) -> (Var b a -> f (Var b b)) -> f (Var b b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Var b a
v -> case Var b a
v of
    B b
b -> Var b b -> f (Var b b)
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> Var b b
forall b a. b -> Var b a
B b
b)
    F a
a -> Scope b f b -> f (Var b b)
forall b (f :: * -> *) a. Scope b f a -> f (Var b a)
unscope (a -> Scope b f b
f a
a)
  {-# INLINE (>>=) #-}


-- | @'substitute' a p w@ replaces the free variable @a@ with @p@ in @w@.
--
-- >>> substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]
-- ["goodnight","Gracie","!!!"]
substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a
substitute :: a -> f a -> f a -> f a
substitute a
a f a
p f a
w = f a
w f a -> (a -> f a) -> f a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
b -> if a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b then f a
p else a -> f a
forall (m :: * -> *) a. Monad m => a -> m a
return a
b
{-# INLINE substitute #-}

-- | @'substituteVar' a b w@ replaces a free variable @a@ with another free variable @b@ in @w@.
--
-- >>> substituteVar "Alice" "Bob" ["Alice","Bob","Charlie"]
-- ["Bob","Bob","Charlie"]
substituteVar :: (Functor f, Eq a) => a -> a -> f a -> f a
substituteVar :: a -> a -> f a -> f a
substituteVar a
a a
p = (a -> a) -> f a -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
b -> if a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b then a
p else a
b)
{-# INLINE substituteVar #-}

-- | Capture some free variables in an expression to yield
-- a 'Scope' with bound variables in @b@
--
-- >>> :m + Data.List
-- >>> abstract (`elemIndex` "bar") "barry"
-- Scope [B 0,B 1,B 2,B 2,F 'y']
abstract :: Functor f => (a -> Maybe b) -> f a -> Scope b f a
abstract :: (a -> Maybe b) -> f a -> Scope b f a
abstract a -> Maybe b
f f a
e = f (Var b a) -> Scope b f a
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope ((a -> Var b a) -> f a -> f (Var b a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Var b a
k f a
e) where
  k :: a -> Var b a
k a
y = case a -> Maybe b
f a
y of
    Just b
z  -> b -> Var b a
forall b a. b -> Var b a
B b
z
    Maybe b
Nothing -> a -> Var b a
forall b a. a -> Var b a
F a
y
{-# INLINE abstract #-}

-- | Abstract over a single variable
--
-- >>> abstract1 'x' "xyz"
-- Scope [B (),F 'y',F 'z']
abstract1 :: (Functor f, Eq a) => a -> f a -> Scope () f a
abstract1 :: a -> f a -> Scope () f a
abstract1 a
a = (a -> Maybe ()) -> f a -> Scope () f a
forall (f :: * -> *) a b.
Functor f =>
(a -> Maybe b) -> f a -> Scope b f a
abstract (\a
b -> if a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing)

-- | Enter a scope, instantiating all bound variables
--
-- >>> :m + Data.List
-- >>> instantiate (\x -> [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"
-- "abccy"
instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a
instantiate :: (b -> f a) -> Scope b f a -> f a
instantiate b -> f a
k Scope b f a
e = Scope b f a -> f (Var b a)
forall b (f :: * -> *) a. Scope b f a -> f (Var b a)
unscope Scope b f a
e f (Var b a) -> (Var b a -> f a) -> f a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Var b a
v -> case Var b a
v of
  B b
b -> b -> f a
k b
b
  F a
a -> a -> f a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
{-# INLINE instantiate #-}

-- | Enter a 'Scope' that binds one variable, instantiating it
--
-- >>> instantiate1 "x" $ Scope [B (),F 'y',F 'z']
-- "xyz"
instantiate1 :: Monad f => f a -> Scope n f a -> f a
instantiate1 :: f a -> Scope n f a -> f a
instantiate1 f a
e = (n -> f a) -> Scope n f a -> f a
forall (f :: * -> *) b a.
Monad f =>
(b -> f a) -> Scope b f a -> f a
instantiate (f a -> n -> f a
forall a b. a -> b -> a
const f a
e)
{-# INLINE instantiate1 #-}

hoistScope :: (f (Var b a) -> g (Var b a)) -> Scope b f a -> Scope b g a
hoistScope :: (f (Var b a) -> g (Var b a)) -> Scope b f a -> Scope b g a
hoistScope f (Var b a) -> g (Var b a)
f = g (Var b a) -> Scope b g a
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope (g (Var b a) -> Scope b g a)
-> (Scope b f a -> g (Var b a)) -> Scope b f a -> Scope b g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Var b a) -> g (Var b a)
f (f (Var b a) -> g (Var b a))
-> (Scope b f a -> f (Var b a)) -> Scope b f a -> g (Var b a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scope b f a -> f (Var b a)
forall b (f :: * -> *) a. Scope b f a -> f (Var b a)
unscope
{-# INLINE hoistScope #-}

-- | Perform a change of variables on bound variables.
mapBound :: Functor f => (b -> b') -> Scope b f a -> Scope b' f a
mapBound :: (b -> b') -> Scope b f a -> Scope b' f a
mapBound b -> b'
f (Scope f (Var b a)
s) = f (Var b' a) -> Scope b' f a
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope ((Var b a -> Var b' a) -> f (Var b a) -> f (Var b' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Var b a -> Var b' a
forall a. Var b a -> Var b' a
f' f (Var b a)
s) where
  f' :: Var b a -> Var b' a
f' (B b
b) = b' -> Var b' a
forall b a. b -> Var b a
B (b -> b'
f b
b)
  f' (F a
a) = a -> Var b' a
forall b a. a -> Var b a
F a
a
{-# INLINE mapBound #-}


-- | Return a list of occurences of the variables bound by this 'Scope'.
bindings :: Foldable f => Scope b f a -> [b]
bindings :: Scope b f a -> [b]
bindings (Scope f (Var b a)
s) = (Var b a -> [b] -> [b]) -> [b] -> f (Var b a) -> [b]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Var b a -> [b] -> [b]
forall a a. Var a a -> [a] -> [a]
f [] f (Var b a)
s where
  f :: Var a a -> [a] -> [a]
f (B a
v) [a]
vs = a
v a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
vs
  f Var a a
_ [a]
vs     = [a]
vs
{-# INLINE bindings #-}

-- | If a term has no free variables, you can freely change the type of
-- free variables it is parameterized on.
--
-- >>> closed [12]
-- Nothing
--
-- >>> closed ""
-- Just []
--
-- >>> :t closed ""
-- closed "" :: Maybe [b]
closed :: Traversable f => f a -> Maybe (f b)
closed :: f a -> Maybe (f b)
closed = (a -> Maybe b) -> f a -> Maybe (f b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Maybe b -> a -> Maybe b
forall a b. a -> b -> a
const Maybe b
forall a. Maybe a
Nothing)
{-# INLINE closed #-}

-- | A closed term has no free variables.
--
-- >>> isClosed []
-- True
--
-- >>> isClosed [1,2,3]
-- False
isClosed :: Foldable f => f a -> Bool
isClosed :: f a -> Bool
isClosed = (a -> Bool) -> f a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> a -> Bool
forall a b. a -> b -> a
const Bool
False)
{-# INLINE isClosed #-}