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(..), String)
  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, showChar, 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                 showsUnaryWith "Abstraction" d $
  86                         (Lift1 `fmap`) `fmap` e
  87 instance (Functor expr, Show bound, Show1 expr, Show var)
  88  => Show (Abstraction bound expr var) where
  89         showsPrec = showsPrec1
  90 instance Monad expr => Applicative (Abstraction bound expr) where
  91         pure  = return
  92         (<*>) = ap
  93 -- | A 'Monad' instance capturing the notion of /variable substitution/,
  94 -- used by 'unabstract' to decrement the /DeBruijn indices/.
  95 instance Monad expr => Monad (Abstraction bound expr) where
  96         return = Abstraction . return . Var_Free . return
  97         Abstraction expr >>= f = Abstraction $ expr >>= \var ->
  98                 case var of
  99                  Var_Bound bound -> return (Var_Bound bound)
 100                  Var_Free  e     -> e >>= (\(Abstraction ex) -> ex) . f
 101 instance MonadTrans (Abstraction bound) where
 102         lift = Abstraction . return . Var_Free
 103 -- | 'Monad_Module_Left' instance capturing the notion
 104 -- of /variable substitution/ with /capture-avoiding/.
 105 instance Monad_Module_Left (Abstraction bound) where
 106         l >>>= f = l >>= lift . f
 107
 108 -- | WARNING: 'abstract' 'fmap'-s the given expression,
 109 -- thus repetitive 'abstract'-ings have a quadratic time-complexity.
 110 abstract
 111  :: Monad expr
 112  => (var -> Maybe bound)
 113  -> expr var
 114  -> Abstraction bound expr var
 115 abstract f = Abstraction . fmap (\var ->
 116         case f var of
 117          Nothing -> Var_Free (return var)
 118          Just b  -> Var_Bound b)
 119
 120 unabstract
 121  :: Monad expr
 122  => (bound -> expr var)
 123  -> Abstraction bound expr var
 124  -> expr var
 125 unabstract unbound (Abstraction ex) = ex >>= \var ->
 126         case var of
 127          Var_Bound b -> unbound b
 128          Var_Free  v -> v
 129
 130 -- | @'abstract_normalize'@ normalize
 131 -- the possible placements of 'Var_Free' in 'Abstraction'
 132 -- by moving them all to the leaves of the 'abstract'-ed expression.
 133 --
 134 -- This gives /traditional DeBruijn indices/ for /bound variables/.
 135 abstract_normalize
 136  :: Monad expr
 137  => Abstraction bound expr var
 138  -> expr (Var bound var)
 139 abstract_normalize (Abstraction expr) = expr >>= \var ->
 140         case var of
 141          Var_Bound bound -> return $ Var_Bound bound
 142          Var_Free  e     -> Var_Free `fmap`{-on var of expr-} e
 143
 144 -- | Convert from /traditional DeBruijn indices/
 145 -- to /generalized DeBruijn indices/,
 146 -- by wrapping all the leaves within the 'Monad'
 147 -- of the given expression.
 148 --
 149 -- This requires a full traversal of the given expression.
 150 abstract_generalize
 151  :: Monad expr
 152  => expr (Var bound var)
 153  -> Abstraction bound expr var
 154 abstract_generalize = Abstraction .
 155         ((return{-of expr-}
 156          `fmap`{-on var of Var-})
 157          `fmap`{-on var of expr-})
 158
 159 -- ** Class 'Monad_Module_Left'
 160 -- | Like ('>>=') but whose 'Monad' is within a wrapping type @left@
 161 -- (aka. /left module over a monad/).
 162 --
 163 -- __Laws:__
 164 --
 165 -- ('>>>=') should satisfy the following equations
 166 -- in order to be used within a 'Monad' instance:
 167 --
 168 -- @
 169 -- ('>>>=' 'return') = id
 170 -- ('>>>=' (('>>=' g) . f)) = ('>>>=' f) . ('>>>=' g)
 171 -- @
 172 --
 173 -- If @left@ has a 'MonadTrans' instance, then:
 174 --
 175 -- @
 176 -- ('>>>=' f) = ('>>=' ('lift' . f))
 177 -- @
 178 --
 179 -- which implies the above equations,
 180 -- see 'MonadTrans' instance of ('Abstraction' @bound@).
 181 --
 182 -- __Uses:__
 183 --
 184 -- * Useful for expression constructors containing 'Abstraction' data.
 185 --
 186 -- __Ressources:__
 187 --
 188 -- * André Hirschowitz, Marco Maggesi, /Modules over monads and initial semantics/.
 189 --   Information and Computation 208 (2010), pp. 545-564,
 190 --   http://www.sciencedirect.com/science/article/pii/S0890540109002405
 191 class Monad_Module_Left left where
 192   (>>>=) :: Monad expr
 193          => left expr var
 194          -> (var -> expr bound)
 195          -> left expr bound
 196 infixl 1 >>>=
 197
 198 -- ** Type 'Var'
 199
 200 -- | 'Var' @bound@ @var@: a variable segregating between:
 201 --
 202 -- * 'Var_Bound', containing data of type @bound@,
 203 --   considered /bound/ by the first enclosing 'Abstraction',
 204 --   hence playing the role of a @Zero@ in /DeBruijn indexing/ terminology.
 205 --
 206 --   Note that the presence of this @bound@ enables the substitution
 207 --   of a 'Var_Bound' by different values,
 208 --   which is used to keep the 'Var_Name' given in the source code,
 209 --   (note that it could also be used to implement a @recursive-let@).
 210 --
 211 -- * 'Var_Free', containing data of type @var@,
 212 --   considered /free/ with respect to the first enclosing 'Abstraction',
 213 --   hence playing the role of a @Succ@ in /DeBruijn indexing/ terminology.
 214 --
 215 --   Note that @var@ is not constrained to be itself a 'Var',
 216 --   this in order to make it possible in 'Abstraction'
 217 --   to insert @expr@ in between the @Succ@ nesting,
 218 --   which optimizes the /DeBruijn indexing/ when 'unabstract'-ing,
 219 --   by avoiding to traverse ('fmap') an @expr@ to @Succ@ its variables
 220 --   (see instance 'MonadTrans' for 'Abstraction').
 221 data Var bound var
 222  =   Var_Bound bound -- ^ @Zero@
 223  |   Var_Free  var -- ^ @Succ@
 224  deriving (Eq, Foldable, Functor, Ord, Show, Traversable)
 225 instance (Buildable bound, Buildable var) => Buildable (Var bound var) where
 226         build var =
 227                 case var of
 228                  Var_Bound b -> build b
 229                  Var_Free  f -> build f
 230
 231 -- | A convenient operator for 'abstract'-ing.
 232 (=?) :: Eq a => a -> a -> Maybe (Suggest a)
 233 (=?) x y = if x == y then Just (Suggest x) else Nothing
 234
 235 -- | A convenient type synonym for clarity.
 236 type Var_Name = Text
 237
 238 -- | A convenient class synonym for brievety.
 239 class (Show var, Buildable var) => Variable var
 240 instance Variable Var_Name
 241 instance (Variable bound, Variable var) => Variable (Var bound var)
 242 instance Variable var => Variable (Suggest var)
 243
 244 -- * Higher-order @Prelude@ classes
 245
 246 -- ** Class 'Eq1'
 247 -- | Lift the 'Eq' class to unary type constructors,
 248 -- 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 -- * /base/ 'Data.Functor.Classes', Ross Paterson, 2013,
 257 --   https://hackage.haskell.org/package/base/docs/Data-Functor-Classes.html
 258 class Eq1 f where
 259         (==#) :: (Eq a, Show a) => f a -> f a -> Bool
 260
 261 class Eq1 f => Ord1 f where
 262         compare1 :: Ord a => f a -> f a -> Ordering
 263
 264 -- ** Class 'Show1'
 265 -- | Lift the 'Show' class to unary type constructors,
 266 -- to avoid the @UndecidableInstances@ language extension.
 267 class Show1 f where
 268         showsPrec1 :: Show a => Int -> f a -> ShowS
 269
 270 showsUnaryWith :: (Show1 f, Show a) => String -> Int -> f a -> ShowS
 271 showsUnaryWith name d x =
 272         showParen (d > 10) $
 273         showString name . showChar ' ' . showsPrec1 11 x
 274
 275 -- ** Type 'Lift1'
 276 -- | Lift the 'Lift' class to unary type constructors,
 277 -- to avoid the @UndecidableInstances@ language extension.
 278 newtype Lift1 f a = Lift1 { lower1 :: f a }
 279         deriving (Functor, Foldable, Traversable, Eq1, Ord1, Show1)
 280 instance (Eq1 f, Eq a, Show a) => Eq   (Lift1 f a) where (==) = (==#)
 281 instance (Ord1 f, Ord a, Show a) => Ord (Lift1 f a) where compare = compare1
 282 instance (Show1 f, Show a) => Show (Lift1 f a) where showsPrec = showsPrec1
 283
 284 -- ** Type 'Suggest'
 285
 286 -- | A convenient wrapper to include data ignored by /α-equivalence/.
 287 newtype Suggest n
 288  =      Suggest n
 289  deriving (Functor, Show)
 290 -- | Always return 'True', in order to be transparent for 'alpha_equiv'.
 291 instance Eq (Suggest n) where
 292         _ == _ = True
 293 instance Ord (Suggest n) where
 294         _ `compare` _ = EQ
 295 instance Buildable var
 296  =>      Buildable (Suggest var) where
 297         build (Suggest var) = build var
 298 instance IsString x => IsString (Suggest x) where
 299         fromString = Suggest . fromString