calculus/Calculus/Abstraction/DeBruijn/Generalized.hs

   1 {-# LANGUAGE DeriveFoldable #-}
   2 {-# LANGUAGE DeriveFunctor #-}
   3 {-# LANGUAGE DeriveTraversable #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
   6 {-# LANGUAGE NoImplicitPrelude #-}
   7 {-# OPTIONS_GHC -fno-warn-tabs #-}
   8 module Calculus.Abstraction.DeBruijn.Generalized where
   9
  10 import Control.Applicative (Applicative(..))
  11 import Control.Monad
  12 import Control.Monad.Trans.Class (MonadTrans(..))
  13 import Data.Bool (Bool(..))
  14 import Data.Eq (Eq(..))
  15 import Data.Foldable (Foldable(..))
  16 import Data.Function (($), (.))
  17 import Data.Function (on)
  18 import Data.Maybe (Maybe(..))
  19 import Data.Ord (Ord(..), Ordering(..))
  20 import Data.String (IsString(..))
  21 import Data.Text (Text)
  22 import Data.Text.Buildable (Buildable(..))
  23 import Data.Traversable (Traversable(..))
  24 import Prelude (Int)
  25 import Text.Show (Show(..), ShowS, showParen, showString)
  26
  27 -- * Type 'Abstraction'
  28 -- | 'Abstraction' @bound@ @expr@ @var@:
  29 -- encodes an 'abstract'-ion
  30 -- over an expression of type @expr@,
  31 -- by segretating its variables between:
  32 --
  33 -- * /bound variables/ of type: @bound@,
  34 -- * and /unbound variables/ (aka. /free variables/) of type: @var@.
  35 --
  36 -- Note that /unbound variables/ may later themselves be made /bound variables/
  37 -- of an enclosing 'Abstraction', effectively encoding
  38 -- /DeBruijn indices/ using Haskell’s /data constructors/,
  39 -- that is, not like in a /traditional DeBruijn indexing/:
  40 -- where an integer is used in each /bound variable/
  41 -- to indicate which one of its enclosing 'Abstraction's is bounding it,
  42 -- but by the nesting of 'Var_Free' data constructors.
  43 -- As a side note, this is also different from the /DeBruijn indexing/
  44 -- encoded at Haskell’s /type level/ by using @GADTs@
  45 -- (done for instance in https://hackage.haskell.org/package/glambda ).
  46 --
  47 -- Moreover, /unbound variables/ are wrapped within a second level of expression
  48 -- in order to improve the time complexity of /traditional DeBruijn indexing/
  49 -- when 'unabstract'-ing (aka. /instantiating/)
  50 -- (see 'Var' and instance 'MonadTrans' of 'Abstraction').
  51 --
  52 -- 'Abstraction' enables:
  53 --
  54 -- * /locally-nameless/ variables (nameless in 'Var_Bound', named in the deepest 'Var_Free');
  55 -- * substitution of /bound variables/ in an expression using /DeBruijn indices/
  56 --   (hence enabling capture-avoiding /β-reduction/
  57 --   and reducing /α-equivalence/ to a structural equality (==));
  58 -- * shifting /DeBruijn indices/ within an expression without traversing it
  59 --   (hence generalizing and speeding up /traditional DeBruijn indices/);
  60 -- * simultaneous substitution of several /bound variables/
  61 --   (hence enabling expressions implementing recursive-@let@).
  62 --
  63 -- __Ressources:__
  64 --
  65 -- * /Bound/, Edward Kmett, 19 August 2013,
  66 --   https://www.schoolofhaskell.com/user/edwardk/bound
  67 newtype Abstraction bound expr var
  68  =      Abstraction (expr (Var bound (expr var)))
  69  deriving (Foldable, Functor, Traversable)
  70 instance (Monad expr, Eq bound, Eq1 expr, Show bound)
  71  => Eq1 (Abstraction bound expr) where
  72         (==#) = (==#) `on` abstract_normalize
  73 instance (Monad expr, Eq bound, Eq1 expr, Eq var, Show var, Show bound)
  74  => Eq (Abstraction bound expr var) where
  75         (==) = (==#)
  76 instance (Monad expr, Ord bound, Ord1 expr, Show bound)
  77  => Ord1 (Abstraction bound expr) where
  78         compare1 = compare1 `on` abstract_normalize
  79 instance (Monad expr, Ord bound, Ord1 expr, Ord var, Show var, Show bound)
  80  => Ord (Abstraction bound expr var) where
  81         compare = compare1
  82 instance (Functor expr, Show bound, Show1 expr)
  83  => Show1 (Abstraction bound expr) where
  84         showsPrec1 d (Abstraction e) =
  85                 showParen (d > 10) $
  86                 showString "Abstraction " .
  87                 showsPrec1 11 ((Lift1 `fmap`) `fmap` e)
  88 instance (Functor expr, Show bound, Show1 expr, Show var)
  89  => Show (Abstraction bound expr var) where
  90         showsPrec = showsPrec1
  91 instance Monad expr => Applicative (Abstraction bound expr) where
  92         pure  = return
  93         (<*>) = ap
  94 -- | A 'Monad' instance capturing the notion of /variable substitution/,
  95 -- used by 'unabstract' to decrement the /DeBruijn indices/.
  96 instance Monad expr => Monad (Abstraction bound expr) where
  97         return = Abstraction . return . Var_Free . return
  98         Abstraction expr >>= f = Abstraction $ expr >>= \var ->
  99                 case var of
 100                  Var_Bound bound -> return (Var_Bound bound)
 101                  Var_Free  e     -> e >>= (\(Abstraction ex) -> ex) . f
 102 instance MonadTrans (Abstraction bound) where
 103         lift = Abstraction . return . Var_Free
 104 -- | 'Monad_Module_Left' instance capturing the notion
 105 -- of /variable substitution/ with /capture-avoiding/.
 106 instance Monad_Module_Left (Abstraction bound) where
 107         l >>>= f = l >>= lift . f
 108
 109 -- | WARNING: 'abstract' 'fmap'-s the given expression,
 110 -- thus repetitive 'abstract'-ings have a quadratic time-complexity.
 111 abstract
 112  :: Monad expr
 113  => (var -> Maybe bound)
 114  -> expr var
 115  -> Abstraction bound expr var
 116 abstract f = Abstraction . fmap (\var ->
 117         case f var of
 118          Nothing -> Var_Free (return var)
 119          Just b  -> Var_Bound b)
 120
 121 unabstract
 122  :: Monad expr
 123  => (bound -> expr var)
 124  -> Abstraction bound expr var
 125  -> expr var
 126 unabstract unbound (Abstraction ex) = ex >>= \var ->
 127         case var of
 128          Var_Bound b -> unbound b
 129          Var_Free  v -> v
 130
 131 -- | @'abstract_normalize'@ normalize
 132 -- the possible placements of 'Var_Free' in 'Abstraction'
 133 -- by moving them all to the leaves of the 'abstract'-ed expression.
 134 --
 135 -- This gives /traditional DeBruijn indices/ for /bound variables/.
 136 abstract_normalize
 137  :: Monad expr
 138  => Abstraction bound expr var
 139  -> expr (Var bound var)
 140 abstract_normalize (Abstraction expr) = expr >>= \var ->
 141         case var of
 142          Var_Bound bound -> return $ Var_Bound bound
 143          Var_Free  e     -> Var_Free `fmap`{-on var of expr-} e
 144
 145 -- | Convert from /traditional DeBruijn indices/
 146 -- to /generalized DeBruijn indices/,
 147 -- by wrapping all the leaves within the 'Monad'
 148 -- of the given expression.
 149 --
 150 -- This requires a full traversal of the given expression.
 151 abstract_generalize
 152  :: Monad expr
 153  => expr (Var bound var)
 154  -> Abstraction bound expr var
 155 abstract_generalize = Abstraction .
 156         ((return{-of expr-}
 157          `fmap`{-on var of Var-})
 158          `fmap`{-on var of expr-})
 159
 160 -- ** Class 'Monad_Module_Left'
 161 -- | Like ('>>=') but whose 'Monad' is within a wrapping type @left@
 162 -- (aka. /left module over a monad/).
 163 --
 164 -- __Laws:__
 165 --
 166 -- ('>>>=') should satisfy the following equations
 167 -- in order to be used within a 'Monad' instance:
 168 --
 169 -- @
 170 -- ('>>>=' 'return') = id
 171 -- ('>>>=' (('>>=' g) . f)) = ('>>>=' f) . ('>>>=' g)
 172 -- @
 173 --
 174 -- If @left@ has a 'MonadTrans' instance, then:
 175 --
 176 -- @
 177 -- ('>>>=' f) = ('>>=' ('lift' . f))
 178 -- @
 179 --
 180 -- which implies the above equations,
 181 -- see 'MonadTrans' instance of ('Abstraction' @bound@).
 182 --
 183 -- __Uses:__
 184 --
 185 -- * Useful for expression constructors containing 'Abstraction' data.
 186 --
 187 -- __Ressources:__
 188 --
 189 -- * André Hirschowitz, Marco Maggesi, /Modules over monads and initial semantics/.
 190 --   Information and Computation 208 (2010), pp. 545-564,
 191 --   http://www.sciencedirect.com/science/article/pii/S0890540109002405
 192 class Monad_Module_Left left where
 193   (>>>=) :: Monad expr
 194          => left expr var
 195          -> (var -> expr bound)
 196          -> left expr bound
 197 infixl 1 >>>=
 198
 199 -- ** Type 'Var'
 200
 201 -- | 'Var' @bound@ @var@: a variable segregating between:
 202 --
 203 -- * 'Var_Bound', containing data of type @bound@,
 204 --   considered /bound/ by the first enclosing 'Abstraction',
 205 --   hence playing the role of a @Zero@ in /DeBruijn indexing/ terminology.
 206 --
 207 --   Note that the presence of this @bound@ enables the substitution
 208 --   of a 'Var_Bound' by different values,
 209 --   which is used to keep the 'Var_Name' given in the source code,
 210 --   (note that it could also be used to implement a @recursive-let@).
 211 --
 212 -- * 'Var_Free', containing data of type @var@,
 213 --   considered /free/ with respect to the first enclosing 'Abstraction',
 214 --   hence playing the role of a @Succ@ in /DeBruijn indexing/ terminology.
 215 --
 216 --   Note that @var@ is not constrained to be itself a 'Var',
 217 --   this in order to make it possible in 'Abstraction'
 218 --   to insert @expr@ in between the @Succ@ nesting,
 219 --   which optimizes the /DeBruijn indexing/ when 'unabstract'-ing,
 220 --   by avoiding to traverse ('fmap') an @expr@ to @Succ@ its variables
 221 --   (see instance 'MonadTrans' for 'Abstraction').
 222 data Var bound var
 223  =   Var_Bound bound -- ^ @Zero@
 224  |   Var_Free  var -- ^ @Succ@
 225  deriving (Eq, Foldable, Functor, Ord, Show, Traversable)
 226 instance (Buildable bound, Buildable var) => Buildable (Var bound var) where
 227         build var =
 228                 case var of
 229                  Var_Bound b -> build b
 230                  Var_Free  f -> build f
 231
 232 -- | A convenient operator for 'abstract'-ing.
 233 (=?) :: Eq a => a -> a -> Maybe (Suggest a)
 234 (=?) x y = if x == y then Just (Suggest x) else Nothing
 235
 236 -- | A convenient type synonym for clarity.
 237 type Var_Name = Text
 238
 239 -- | A convenient class synonym for brievety.
 240 class (Show var, Buildable var) => Variable var
 241 instance Variable Var_Name
 242 instance (Variable bound, Variable var) => Variable (Var bound var)
 243 instance Variable var => Variable (Suggest var)
 244
 245 -- * Higher-order @Prelude@ classes
 246
 247 -- ** Class 'Eq1'
 248 -- | Higher-order 'Eq' to avoid the @UndecidableInstances@ language extension.
 249 --
 250 -- __Ressources:__
 251 --
 252 -- * /Simulating Quantified Class Constraints/, Valery Trifonov, 2003,
 253 --   http://flint.cs.yale.edu/trifonov/papers/sqcc.pdf
 254 -- * /prelude-extras/, Edward Kmett, 2011,
 255 --   https://hackage.haskell.org/package/prelude-extras
 256 class Eq1 f where
 257         (==#) :: (Eq a, Show a) => f a -> f a -> Bool
 258
 259 class Eq1 f => Ord1 f where
 260         compare1 :: Ord a => f a -> f a -> Ordering
 261
 262 -- ** Class 'Show1'
 263 -- | Higher-order 'Show' to avoid the @UndecidableInstances@ language extension.
 264 class Show1 f where
 265         showsPrec1 :: Show a => Int -> f a -> ShowS
 266
 267 -- ** Type 'Lift1'
 268 -- | Higher-order 'Lift' to avoid the @UndecidableInstances@ language extension.
 269 newtype Lift1 f a = Lift1 { lower1 :: f a }
 270         deriving (Functor, Foldable, Traversable, Eq1, Ord1, Show1)
 271 instance (Eq1 f, Eq a, Show a) => Eq   (Lift1 f a) where (==) = (==#)
 272 instance (Ord1 f, Ord a, Show a) => Ord (Lift1 f a) where compare = compare1
 273 instance (Show1 f, Show a) => Show (Lift1 f a) where showsPrec = showsPrec1
 274
 275 -- ** Type 'Suggest'
 276
 277 -- | A convenient wrapper to include data ignored by /α-equivalence/.
 278 newtype Suggest n
 279  =      Suggest n
 280  deriving (Functor, Show)
 281 -- | Always return 'True', in order to be transparent for 'alpha_equiv'.
 282 instance Eq (Suggest n) where
 283         _ == _ = True
 284 instance Ord (Suggest n) where
 285         _ `compare` _ = EQ
 286 instance Buildable var
 287  =>      Buildable (Suggest var) where
 288         build (Suggest var) = build var
 289 instance IsString x => IsString (Suggest x) where
 290         fromString = Suggest . fromString