{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DerivingStrategies #-}
{-# language DeriveAnyClass #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# language CPP #-}
{-# options_ghc -Wno-unused-top-binds #-}

{-|
Module      : Bound.Simple
Description : Lightweight implementation of 'bound'
Copyright   : (c) 2013 Edward Kmett, 2021 Marco Zocca
License     : BSD
Maintainer  : github.com/ocramz
Stability   : experimental
Portability : POSIX

= 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'. This works on most recent versions of GHC (>= 8.6.1).

Note 2 : the example below requires language extensions `DeriveFunctor`, `DeriveFoldable`, `DeriveTraversable` and `DerivingVia`.

@
import Bound.Simple (Scope, Bound(..), abstract1, instantiate1)
import Data.Functor.Classes (Show1)
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 #-}