src/Symantic/Typed/Optim.hs

   1 module Symantic.Typed.Optim where
   2
   3 import qualified Data.Function as Fun
   4 import Symantic.Typed.Lang
   5 import Symantic.Typed.Data
   6
   7 -- | Beta-reduce the left-most outer-most lambda abstraction (aka. normal-order reduction),
   8 -- but to avoid duplication of work, only those manually marked
   9 -- as using their variable at most once.
  10 --
  11 -- DOC: Demonstrating Lambda Calculus Reduction, Peter Sestoft, 2001,
  12 -- https://www.itu.dk/people/sestoft/papers/sestoft-lamreduce.pdf
  13 normalOrderReduction :: forall repr a.
  14   Abstractable repr =>
  15   SomeData repr a -> SomeData repr a
  16 normalOrderReduction = nor
  17   where
  18   -- | normal-order reduction
  19   nor :: SomeData repr b -> SomeData repr b
  20   nor = \case
  21     Data (Lam f) -> lam (nor Fun.. f)
  22     Data (Lam1 f) -> lam1 (nor Fun.. f)
  23     Data (x :@ y) -> case whnf x of
  24       Data (Lam1 f) -> nor (f y)
  25       x' -> nor x' .@ nor y
  26     x -> x
  27   -- | weak-head normal-form
  28   whnf :: SomeData repr b -> SomeData repr b
  29   whnf = \case
  30     Data (x :@ y) -> case whnf x of
  31       Data (Lam1 f) -> whnf (f y)
  32       x' -> x' .@ y
  33     x -> x