{-# LANGUAGE CPP
, ScopedTypeVariables
, GADTs
, DataKinds
, PolyKinds
, TypeOperators
, Rank2Types
, MultiParamTypeClasses
, FlexibleContexts
, FlexibleInstances
, FunctionalDependencies
, UndecidableInstances
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Syntax.ABT
(
module Language.Hakaru.Syntax.Variable
, resolveVar
, View(..)
, unviewABT
, ABT(..)
, caseVarSyn
, binds
, binds_
, caseBinds
, underBinders
, maxNextFree
, maxNextBind
, maxNextFreeOrBind
, rename
, renames
, subst
, substM
, substs
, binder
, binderM
, Binders(binders)
, withMetadata
, cataABT
, cataABTM
, paraABT
, TrivialABT()
, MemoizedABT()
, MetaABT(..)
) where
import Data.Text (Text, empty)
import qualified Data.Foldable as F
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative hiding (empty)
import Data.Monoid (Monoid(..))
#endif
import Control.Monad
import Control.Monad.Identity
import Control.Monad.Fix
import Data.Number.Nat
import Language.Hakaru.Syntax.IClasses
import Language.Hakaru.Types.Sing
import Language.Hakaru.Syntax.Variable
#ifdef __TRACE_DISINTEGRATE__
import Debug.Trace (trace)
#endif
data View :: (k -> *) -> [k] -> k -> * where
Syn :: !(rec a) -> View rec '[] a
-- A variable use.
Var :: {-# UNPACK #-} !(Variable a) -> View rec '[] a
-- N.B., this constructor is recursive, thus minimizing the
-- memory overhead of whatever annotations our ABT stores (we
-- only annotate once, at the top of a chaing of 'Bind's, rather
-- than before each one). However, in the 'ABT' class, we provide
-- an API as if things went straight back to @abt@. Doing so
-- requires that 'caseBind' is part of the class so that we
-- can push whatever annotations down over one single level of
-- 'Bind', rather than pushing over all of them at once and
-- then needing to reconstruct all but the first one.
--
-- A variable binding.
Bind
:: {-# UNPACK #-} !(Variable a)
-> !(View rec xs b)
-> View rec (a ': xs) b
instance Functor12 View where
fmap12 f (Syn t) = Syn (f t)
fmap12 _ (Var x) = Var x
fmap12 f (Bind x e) = Bind x (fmap12 f e)
instance Foldable12 View where
foldMap12 f (Syn t) = f t
foldMap12 f (Var x) = mempty
foldMap12 f (Bind x e) = foldMap12 f e
instance Traversable12 View where
traverse12 f (Syn t) = Syn <$> f t
traverse12 _ (Var x) = pure $ Var x
traverse12 f (Bind x e) = Bind x <$> traverse12 f e
instance (Show1 (Sing :: k -> *), Show1 rec)
=> Show2 (View (rec :: k -> *))
where
showsPrec2 p (Syn t) = showParen_1 p "Syn" t
showsPrec2 p (Var x) = showParen_1 p "Var" x
showsPrec2 p (Bind x v) = showParen_12 p "Bind" x v
instance (Show1 (Sing :: k -> *), Show1 rec)
=> Show1 (View (rec :: k -> *) xs)
where
showsPrec1 = showsPrec2
show1 = show2
-- TODO: could weaken the Show1 requirements to Show requirements...
instance (Show1 (Sing :: k -> *), Show1 rec)
=> Show (View (rec :: k -> *) xs a)
where
showsPrec = showsPrec1
show = show1
-- TODO: neelk includes 'subst' as a method. Any reason we should?
-- TODO: jon includes instantiation as a method. Any reason we should?
-- TODO: require @(JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Foldable21 syn)@ since all our instances will need those too?
--
-- | The class interface for abstract binding trees. The first
-- argument, @syn@, gives the syntactic signature of the ABT;
-- whereas, the second argument, @abt@, is thing being declared as
-- an ABT for @syn@. The first three methods ('syn', 'var', 'bind')
-- alow us to inject any 'View' into the @abt@. The other methods
-- provide various views for extracting information from the @abt@.
--
-- At present we're using fundeps in order to restrict the relationship
-- between @abt@ and @syn@. However, in the future we may move @syn@
-- into being an associated type, if that helps to clean things up
-- (since fundeps and type families don't play well together). The
-- idea behind the fundep is that certain @abt@ implementations may
-- only be able to work for particular @syn@ signatures. This isn't
-- the case for 'TrivialABT' nor 'MemoizedABT', but isn't too
-- far-fetched.
class ABT (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *) | abt -> syn where
-- Smart constructors for building a 'View' and then injecting it into the @abt@.
syn :: syn abt a -> abt '[] a
var :: Variable a -> abt '[] a
bind :: Variable a -> abt xs b -> abt (a ': xs) b
-- TODO: better name. "unbind"? "fromBind"?
--
-- When the left side is defined, we have the following laws:
-- > caseBind e bind == e
-- > caseBind (bind x e) k == k x (unviewABT $ viewABT e)
-- However, we do not necessarily have the following:
-- > caseBind (bind x e) k == k x e
-- because the definition of 'caseBind' for 'MemoizedABT'
-- is not exact.
--
-- | Since the first argument to @abt@ is not @'[]@, we know
-- it must be 'Bind'. So we do case analysis on that constructor,
-- pushing the annotation down one binder (but not over the
-- whole recursive 'View' layer).
caseBind :: abt (x ': xs) a -> (Variable x -> abt xs a -> r) -> r
-- See note about exposing 'View', 'viewABT', and 'unviewABT'.
-- We could replace 'viewABT' with a case-elimination version...
viewABT :: abt xs a -> View (syn abt) xs a
freeVars :: abt xs a -> VarSet (KindOf a)
-- | Return the successor of the largest 'varID' of /free/
-- variables. Thus, if there are no free variables we return
-- zero. The default implementation is to take the successor
-- of the maximum of 'freeVars'. This is part of the class in
-- case you want to memoize it.
--
-- This function is used in order to generate guaranteed-fresh
-- variables without the need for a name supply. In particular,
-- it's used to ensure that the generated variable don't capture
-- any free variables in the term.
--
-- * /Default:/ @nextFree = 'nextVarID' . 'freeVars'@
nextFree :: abt xs a -> Nat
nextFree = nextVarID . freeVars
-- | Return the successor of the largest 'varID' of variable
-- /binding sites/ (i.e., of variables bound by the 'Bind'
-- constructor). Thus, if there are no binders, then we will
-- return zero. N.B., this should return zero for /uses/ of the
-- bound variables themselves. This is part of the class in
-- case you want to memoize it.
--
-- This function is used in order to generate guaranteed-fresh
-- variables without the need for a name supply. In particular,
-- it's used to ensure that the generated variable won't be
-- captured or shadowed by bindings already in the term.
nextBind :: abt xs a -> Nat
-- | Return the maximum of 'nextFree' and 'nextBind'. For when
-- you want to be really paranoid about choosing new variable
-- IDs. In principle this shouldn't be necessary since we should
-- always freshen things when going under binders; but for some
-- reason only using 'nextFree' keeps leading to bugs in
-- transformations like disintegration and expectation.
--
-- /N.B./, it is impossible to implement this function such
-- that it is lazy in the bound variables like 'nextBind' is.
-- Thus, it cannot be used for knot-tying tricks like 'nextBind'
-- can.
--
-- * /Default:/ @nextFreeOrBind e = 'nextFree' e `max` 'nextBind' e@
nextFreeOrBind :: abt xs a -> Nat
nextFreeOrBind e = nextFree e `max` nextBind e
-- TODO: add a function for checking alpha-equivalence? Refreshing all variable IDs to be in some canonical form? Other stuff?
-- See note about exposing 'View', 'viewABT', and 'unviewABT'
unviewABT :: (ABT syn abt) => View (syn abt) xs a -> abt xs a
unviewABT (Syn t) = syn t
unviewABT (Var x) = var x
unviewABT (Bind x v) = bind x (unviewABT v)
-- | Since the first argument to @abt@ is @'[]@, we know it must
-- be either 'Syn' of 'Var'. So we do case analysis with those two
-- constructors.
caseVarSyn
:: (ABT syn abt)
=> abt '[] a
-> (Variable a -> r)
-> (syn abt a -> r)
-> r
caseVarSyn e var_ syn_ =
case viewABT e of
Syn t -> syn_ t
Var x -> var_ x
-- | Call 'bind' repeatedly.
binds :: (ABT syn abt) => List1 Variable xs -> abt ys b -> abt (xs ++ ys) b
binds Nil1 e = e
binds (Cons1 x xs) e = bind x (binds xs e)
-- | A specialization of 'binds' for when @ys ~ '[]@. We define
-- this to avoid the need for using 'eqAppendIdentity' on the result
-- of 'binds' itself.
binds_ :: (ABT syn abt) => List1 Variable xs -> abt '[] b -> abt xs b
binds_ Nil1 e = e
binds_ (Cons1 x xs) e = bind x (binds_ xs e)
-- TODO: take a continuation so that the type more closely resembles 'caseBind'; or, remove the CPSing in 'caseBind' so it more closely resembles this
-- | Call 'caseBind' repeatedly. (Actually we use 'viewABT'.)
caseBinds :: (ABT syn abt) => abt xs a -> (List1 Variable xs, abt '[] a)
caseBinds = go . viewABT
where
go :: (ABT syn abt)
=> View (syn abt) xs a -> (List1 Variable xs, abt '[] a)
go (Syn t) = (Nil1, syn t)
go (Var x) = (Nil1, var x)
go (Bind x v) = let ~(xs,e) = go v in (Cons1 x xs, e)
-- TODO: give better name
-- | Transform expression under binds
underBinders
:: (ABT syn abt)
=> (abt '[] a -> abt '[] b)
-> abt xs a
-> abt xs b
underBinders f e =
let (vars, e') = caseBinds e
in binds_ vars (f e')
-- | Call 'nextFree' on all the terms and return the maximum.
maxNextFree :: (ABT syn abt, F.Foldable f) => f (Some2 abt) -> Nat
maxNextFree = unMaxNat . F.foldMap (\(Some2 e) -> MaxNat $ nextFree e)
-- | Call 'nextBind' on all the terms and return the maximum.
maxNextBind :: (ABT syn abt, F.Foldable f) => f (Some2 abt) -> Nat
maxNextBind = unMaxNat . F.foldMap (\(Some2 e) -> MaxNat $ nextBind e)
-- | Call 'nextFreeOrBind' on all the terms and return the maximum.
maxNextFreeOrBind :: (ABT syn abt, F.Foldable f) => f (Some2 abt) -> Nat
maxNextFreeOrBind =
unMaxNat . F.foldMap (\(Some2 e) -> MaxNat $ nextFreeOrBind e)
----------------------------------------------------------------
----------------------------------------------------------------
-- | A trivial ABT with no annotations.
--
-- The 'Show' instance does not expose the raw underlying data
-- types, but rather prints the smart constructors 'var', 'syn',
-- and 'bind'. This makes things prettier, but also means that if
-- you paste the string into a Haskell file you can use it for any
-- 'ABT' instance.
--
-- The 'freeVars', 'nextFree', and 'nextBind' methods are all very
-- expensive for this ABT, because we have to traverse the term
-- every time we want to call them. The 'MemoizedABT' implementation
-- fixes this.
newtype TrivialABT (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k]) (a :: k) =
TrivialABT (View (syn (TrivialABT syn)) xs a)
instance (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Foldable21 syn)
=> ABT (syn :: ([k] -> k -> *) -> k -> *) (TrivialABT syn)
where
syn t = TrivialABT (Syn t)
var x = TrivialABT (Var x)
bind x (TrivialABT v) = TrivialABT (Bind x v)
caseBind (TrivialABT v) k =
case v of
Bind x v' -> k x (TrivialABT v')
viewABT (TrivialABT v) = v
freeVars = go . viewABT
where
go :: View (syn (TrivialABT syn)) xs a
-> VarSet (KindOf a)
go (Syn t) = foldMap21 freeVars t
go (Var x) = singletonVarSet x
go (Bind x v) = deleteVarSet x (go v)
-- N.B., we could make this implementation much faster by
-- avoiding traversing under binders. Under the assumption that
-- the largest binder is the outermost one, this optimization
-- is sound; and indeed the 'binder' function maintains that
-- invariant. (If implementing this optimization, we can
-- distinguish the case of 'Syn' underneath 'Bind' vs a top-level
-- 'Syn' by checking whether the accumulator @n@ is zero or
-- not.) However, if the largest binder is not the outermost
-- one, then it would return the wrong answer. Since the
-- 'TrivialABT' type is mainly intended for testing rather than
-- production use, we avoid using this optimization so as to
-- err on the side of soundness.
nextBind = go . viewABT
where
go :: View (syn (TrivialABT syn)) xs a -> Nat
go (Syn t) = unMaxNat $ foldMap21 (MaxNat . nextBind) t
go (Var _) = unMaxNat $ mempty -- We mustn't look at variable *uses*!
go (Bind x v) = max (1 + varID x) (go v)
-- Deforest the intermediate 'VarSet' of the default 'nextFree'
-- implementation, and fuse the two passes of 'nextFree' and
-- 'nextBind' into a single pass.
nextFreeOrBind = go . viewABT
where
go :: View (syn (TrivialABT syn)) xs a -> Nat
go (Syn t) = unMaxNat $ foldMap21 (MaxNat . nextFreeOrBind) t
go (Var x) = 1 + varID x
go (Bind x v) = max (1 + varID x) (go v)
-- BUG: requires UndecidableInstances
instance (Show1 (Sing :: k -> *), Show1 (syn (TrivialABT syn)))
=> Show2 (TrivialABT (syn :: ([k] -> k -> *) -> k -> *))
where
{-
-- Print the concrete data constructors:
showsPrec2 p (TrivialABT v) =
showParen (p > 9)
( showString "TrivialABT "
. showsPrec1 11 v
)
-}
-- Do something a bit prettier. (Because we print the smart
-- constructors, this output can also be cut-and-pasted to work
-- for any ABT instance.)
showsPrec2 p (TrivialABT (Syn t)) = showParen_1 p "syn" t
showsPrec2 p (TrivialABT (Var x)) = showParen_1 p "var" x
showsPrec2 p (TrivialABT (Bind x v)) = showParen_11 p "bind" x (TrivialABT v)
instance (Show1 (Sing :: k -> *), Show1 (syn (TrivialABT syn)))
=> Show1 (TrivialABT (syn :: ([k] -> k -> *) -> k -> *) xs)
where
showsPrec1 = showsPrec2
show1 = show2
-- TODO: could weaken the Show1 requirements to Show requirements...
instance (Show1 (Sing :: k -> *), Show1 (syn (TrivialABT syn)))
=> Show (TrivialABT (syn :: ([k] -> k -> *) -> k -> *) xs a)
where
showsPrec = showsPrec1
show = show1
----------------------------------------------------------------
-- TODO: replace @VarSet@ with @VarMap Nat@ where the
-- Nat is the number of times the variable occurs. That way, we can
-- tell when a bound variable is unused or only used only once (and
-- hence performing beta\/let reduction would be a guaranteed win),
-- and if it's used more than once then we can use the number of
-- occurances in our heuristic for deciding whether reduction would
-- be a win or not.
--
-- TODO: generalize this pattern for any monoidal annotation?
-- TODO: what is the performance cost of letting 'memoizedFreeVars' be lazy? Is it okay to lose the ability to use 'binder' in order to shore that up?
-- WARNING: in older versions of the library, there was an issue
-- about the memoization of 'nextBind' breaking our ability to
-- tie-the-knot in 'binder'. Everything seems to work now, but it's
-- not entirely clear to me what changed...
-- | An ABT which memoizes 'freeVars', 'nextBind', and 'nextFree',
-- thereby making them take only /O(1)/ time.
--
-- N.B., the memoized set of free variables is lazy so that we can
-- tie-the-knot in 'binder' without interfering with our memos. The
-- memoized 'nextFree' must be lazy for the same reason.
data MemoizedABT (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k]) (a :: k) =
MemoizedABT
{ _memoizedFreeVars :: VarSet (KindOf a) -- N.B., lazy!
, memoizedNextFree :: Nat -- N.B., lazy!
, memoizedNextBind :: {-# UNPACK #-} !Nat
, memoizedView :: !(View (syn (MemoizedABT syn)) xs a)
}
-- HACK: ""Cannot use record selector ‘_memoizedFreeVars’ as a function due to escaped type variables""
memoizedFreeVars :: MemoizedABT syn xs a -> VarSet (KindOf a)
memoizedFreeVars (MemoizedABT xs _ _ _) = xs
instance (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Foldable21 syn)
=> ABT (syn :: ([k] -> k -> *) -> k -> *) (MemoizedABT syn)
where
syn t =
MemoizedABT
(foldMap21 freeVars t)
(unMaxNat $ foldMap21 (MaxNat . nextFree) t)
(unMaxNat $ foldMap21 (MaxNat . nextBind) t)
(Syn t)
var x =
MemoizedABT
(singletonVarSet x)
(1 + varID x)
0
(Var x)
bind x (MemoizedABT xs _ nb v) =
let xs' = deleteVarSet x xs
in MemoizedABT
xs'
(nextVarID xs')
((1 + varID x) `max` nb)
(Bind x v)
-- N.B., when we go under the binder, the variable @x@ may not
-- actually be used, but we add it to the set of freeVars
-- anyways. The reasoning is thus: this function is mainly used
-- in defining 'subst', and for that purpose it's important to
-- track all the variables which /could be/ free, so that we
-- can freshen appropriately. It may be safe to not include @x@
-- when @x@ is not actually used in @v'@, but it's best not to
-- risk it. Moreover, once we add support for open terms (i.e.,
-- truly-free variables) then we'll need to account for the
-- fact that the variable @x@ may come to be used in the grounding
-- of the open term, even though it's not used in the part of
-- the term we already know. Similarly, the true 'nextBind' may
-- be lower now that we're going under this binding; but keeping
-- it the same is an always valid approximation.
--
-- TODO: we could actually compute things exactly, similar to
-- how we do it in 'syn'; but unclear if that's really worth it...
caseBind (MemoizedABT xs nf nb v) k =
case v of
Bind x v' ->
k x $ MemoizedABT
(insertVarSet x xs)
((1 + varID x) `max` nf)
nb
v'
viewABT = memoizedView
freeVars = memoizedFreeVars
nextFree = memoizedNextFree
nextBind = memoizedNextBind
instance (Show1 (Sing :: k -> *), Show1 (syn (MemoizedABT syn)))
=> Show2 (MemoizedABT (syn :: ([k] -> k -> *) -> k -> *))
where
showsPrec2 p (MemoizedABT xs nf nb v) =
showParen (p > 9)
( showString "MemoizedABT "
. showsPrec 11 xs
. showString " "
. showsPrec 11 nf
. showString " "
. showsPrec 11 nb
. showString " "
. showsPrec1 11 v
)
instance (Show1 (Sing :: k -> *), Show1 (syn (MemoizedABT syn)))
=> Show1 (MemoizedABT (syn :: ([k] -> k -> *) -> k -> *) xs)
where
showsPrec1 = showsPrec2
show1 = show2
-- TODO: could weaken the Show1 requirements to Show requirements...
instance (Show1 (Sing :: k -> *), Show1 (syn (MemoizedABT syn)))
=> Show (MemoizedABT (syn :: ([k] -> k -> *) -> k -> *) xs a)
where
showsPrec = showsPrec1
show = show1
----------------------------------------------------------------
-- | An ABT which carries around metadata at each node.
--
-- Right now this essentially inlines the the TrivialABT instance
-- but it would be nice if it was abstract in the choice of ABT.
data MetaABT
(meta :: *)
(syn :: ([k] -> k -> *) -> k -> *)
(xs :: [k])
(a :: k) =
MetaABT
{ getMetadata :: !(Maybe meta)
, metaView :: !(View (syn (MetaABT meta syn)) xs a)
}
withMetadata
:: meta
-> MetaABT meta syn xs a
-> MetaABT meta syn xs a
withMetadata x (MetaABT _ v) = MetaABT (Just x) v
instance (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Foldable21 syn)
=> ABT (syn :: ([k] -> k -> *) -> k -> *) (MetaABT meta syn)
where
syn t = MetaABT Nothing (Syn t)
var x = MetaABT Nothing (Var x)
bind x (MetaABT meta v) = MetaABT meta (Bind x v)
caseBind (MetaABT meta v) k =
case v of
Bind x v' -> k x (MetaABT meta v')
viewABT = metaView
freeVars = go . viewABT
where
go :: View (syn (MetaABT meta syn)) xs a
-> VarSet (KindOf a)
go (Syn t) = foldMap21 freeVars t
go (Var x) = singletonVarSet x
go (Bind x v) = deleteVarSet x (go v)
nextBind = go . viewABT
where
go :: View (syn (MetaABT meta syn)) xs a -> Nat
go (Syn t) = unMaxNat $ foldMap21 (MaxNat . nextBind) t
go (Var _) = unMaxNat $ mempty
go (Bind x v) = max (1 + varID x) (go v)
-- Deforest the intermediate 'VarSet' of the default 'nextFree'
-- implementation, and fuse the two passes of 'nextFree' and
-- 'nextBind' into a single pass.
nextFreeOrBind = go . viewABT
where
go :: View (syn (MetaABT meta syn)) xs a -> Nat
go (Syn t) = unMaxNat $ foldMap21 (MaxNat . nextFreeOrBind) t
go (Var x) = 1 + varID x
go (Bind x v) = max (1 + varID x) (go v)
instance ( Show1 (Sing :: k -> *)
, Show1 (syn (MetaABT meta syn))
, Show meta)
=> Show2 (MetaABT meta (syn :: ([k] -> k -> *) -> k -> *))
where
showsPrec2 p (MetaABT meta v) =
showParen (p > 9)
( showString "MetaABT "
. showsPrec 11 meta
. showString " "
. showsPrec1 11 v
)
instance ( Show1 (Sing :: k -> *)
, Show1 (syn (MetaABT meta syn))
, Show meta)
=> Show1 (MetaABT meta (syn :: ([k] -> k -> *) -> k -> *) xs)
where
showsPrec1 = showsPrec2
show1 = show2
instance ( Show1 (Sing :: k -> *)
, Show1 (syn (MetaABT meta syn))
, Show meta)
=> Show (MetaABT meta (syn :: ([k] -> k -> *) -> k -> *) xs a)
where
showsPrec = showsPrec1
show = show1
----------------------------------------------------------------
----------------------------------------------------------------
-- TODO: do something smarter
-- | If the variable is in the set, then construct a new one which
-- isn't (but keeping the same hint and type as the old variable).
-- If it isn't in the set, then just return it.
freshen
:: (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *))
=> Variable (a :: k)
-> VarSet (KindOf a)
-> Variable a
freshen x xs
| x `memberVarSet` xs = let i = nextVarID xs in i `seq` x{varID = i}
| otherwise = x
-- TODO: reimplement this using 'cataABT' or 'paraABT'. Possibly make
-- strict versions of them in order to match the semantics we already
-- have about throwing 'VarEqTypeError' in a timely manner.
--
-- | Rename a free variable. Does nothing if the variable is bound.
rename
:: forall syn abt (a :: k) xs (b :: k)
. (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Functor21 syn, ABT syn abt)
=> Variable a
-> Variable a
-> abt xs b
-> abt xs b
rename x y =
#ifdef __TRACE_DISINTEGRATE__
trace ("renaming " ++ show (varID x)
++ " to " ++ show (varID y)) $
#endif
start
where
start :: forall xs' b'. abt xs' b' -> abt xs' b'
start e = loop e (viewABT e)
-- TODO: is it actually worth passing around the @e@? Benchmark.
loop :: forall xs' b'. abt xs' b' -> View (syn abt) xs' b' -> abt xs' b'
loop _ (Syn t) = syn $! fmap21 start t
loop e (Var z) =
case varEq x z of
Just Refl -> var y
Nothing -> e
loop e (Bind z v) =
#ifdef __TRACE_DISINTEGRATE__
trace ("checking varEq "++ show (varID x) ++ " " ++ show (varID z)) $
#endif
case varEq x z of
Just Refl -> e
Nothing -> bind z $ loop (caseBind e $ const id) v
-- TODO: reimplement this using 'cataABT' or 'paraABT'. Possibly make
-- strict versions of them in order to match the semantics we already
-- have about throwing 'VarEqTypeError' in a timely manner.
--
-- TODO: keep track of a variable renaming environment, and do
-- renaming on the fly rather than traversing the ABT repeatedly.
--
-- TODO: make an explicit distinction between substitution in general
-- vs instantiation of the top-level bound variable (i.e., the
-- function of type @abt (x ': xs) a -> abt '[] x -> abt xs a@).
-- cf., <http://hackage.haskell.org/package/abt>
--
-- | Perform capture-avoiding substitution. This function will
-- either preserve type-safety or else throw an 'VarEqTypeError'
-- (depending on which interpretation of 'varEq' is chosen). N.B.,
-- to ensure timely throwing of exceptions, the 'Term' and 'ABT'
-- should have strict 'fmap21' definitions.
subst
:: forall syn abt (a :: k) xs (b :: k)
. (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Traversable21 syn, ABT syn abt)
=> Variable a
-> abt '[] a
-> abt xs b
-> abt xs b
subst x e =
#ifdef __TRACE_DISINTEGRATE__
trace ("about to subst " ++ show (varID x)) $
#endif
runIdentity . substM x e varCase
where
varCase :: forall m b'. (Applicative m, Functor m, Monad m)
=> Variable b' -> m (abt '[] b')
varCase = return . var
substM
:: forall syn abt (a :: k) xs (b :: k) m
. (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *),
Traversable21 syn, ABT syn abt,
Applicative m, Functor m, Monad m)
=> Variable a
-> abt '[] a
-> (forall b'. Variable b' -> m (abt '[] b'))
-> abt xs b
-> m (abt xs b)
substM x e vf =
start (maxNextFreeOrBind [Some2 (var x), Some2 e])
where
-- TODO: we could use the director-strings approach to optimize
-- this (for MemoizedABT, but pessimizing for TrivialABT) by first
-- checking whether @x@ is free in @f@; if so then recurse, if not
-- then we're done.
start :: forall xs' b'. Nat -> abt xs' b' -> m (abt xs' b')
start n f = loop n f (viewABT f)
-- TODO: is it actually worth passing around the @f@? Benchmark.
loop :: forall xs' b'
. Nat -> abt xs' b' -> View (syn abt) xs' b' -> m (abt xs' b')
loop n _ (Syn t) = syn <$> traverse21 (start n) t
loop _ f (Var z) =
#ifdef __TRACE_DISINTEGRATE__
trace ("checking varEq " ++ show (varID x) ++ " " ++ show (varID z)) $
#endif
case varEq x z of
Just Refl -> return e
Nothing -> vf z
loop n f (Bind z b) =
if (varID x == varID z) then return f
else do -- TODO: even if we don't come up with a smarter way
-- of freshening variables, it'd be better to just pass
-- both sets to 'freshen' directly and then check them
-- each; rather than paying for taking their union every
-- time we go under a binder like this.
let i = 1 + max n (nextFreeOrBind f) -- (freeVars e `mappend` freeVars f)
z' = i `seq` z{varID = i}
f'' <- substM z (var z') vf (unviewABT b)
bind z' <$> loop i f'' (viewABT f'')
renames
:: forall
(syn :: ([k] -> k -> *) -> k -> *)
(abt :: [k] -> k -> *)
(xs :: [k])
(a :: k)
. ( ABT syn abt
, JmEq1 (Sing :: k -> *)
, Show1 (Sing :: k -> *)
, Functor21 syn
)
=> Assocs (Variable :: k -> *)
-> abt xs a
-> abt xs a
renames rho0 =
-- Guaranteed correct (since 'subst' is correct) but very inefficient
\e0 -> F.foldl (\e (Assoc x v) -> rename x v e) e0 (unAssocs rho0)
{-
-- called (//) in Jon's abt library. We use this textual name so we can also have 'insts' for the n-ary version, rather than iterating the unary version. Or we could use something like (!) and (!!), albeit those names tend to be used to mean other things. It'd be nice to do (@) and (@@), but the first one is illegal.
inst
:: forall syn abt (a :: k) xs (b :: k)
. ( JmEq1 (Sing :: k -> *)
, Show1 (Sing :: k -> *)
, Functor21 syn
, ABT syn abt
)
=> abt (a ': xs) b
-> abt '[] a
-> abt xs b
inst f e =
caseBind f $ \x f' ->
subst x e f'
-}
-- BUG: This appears to have both capture and escape issues as demonstrated by 'Tests.Disintegrate.test0' and commented on at 'Language.Hakaru.Evaluation.Types.runM'.
-- | The parallel version of 'subst' for performing multiple substitutions at once.
substs
:: forall
(syn :: ([k] -> k -> *) -> k -> *)
(abt :: [k] -> k -> *)
(xs :: [k])
(a :: k)
. ( ABT syn abt
, JmEq1 (Sing :: k -> *)
, Show1 (Sing :: k -> *)
, Traversable21 syn
)
=> Assocs (abt '[])
-> abt xs a
-> abt xs a
substs rho0 =
-- Guaranteed correct (since 'subst' is correct) but very inefficient
\e0 -> F.foldl (\e (Assoc x v) -> subst x v e) e0 (unAssocs rho0)
{- -- old buggy version
start rho0
where
fv0 :: VarSet (KindOf a)
fv0 = F.foldMap (\(Assoc _ e) -> freeVars e) (unAssocs rho0)
start :: forall xs' a'. Assocs abt -> abt xs' a' -> abt xs' a'
start rho e = loop rho e (viewABT e)
loop :: forall xs' a'
. Assocs abt -> abt xs' a' -> View (syn abt) xs' a' -> abt xs' a'
loop rho _ (Syn t) = syn $! fmap21 (start rho) t
loop rho e (Var x) =
case IM.lookup (fromNat $ varID x) (unAssocs rho) of
Nothing -> e
Just (Assoc y e') ->
case varEq x y of
Just Refl -> e'
Nothing -> e
loop rho e (Bind x _body) =
case IM.lookup (fromNat $ varID x) (unAssocs rho) of
Nothing -> e
Just (Assoc y _) ->
case varEq x y of
Just Refl ->
let rho' = IM.delete (fromNat $ varID x) (unAssocs rho) in
if IM.null rho'
then e
else caseBind e $ \_x body' ->
bind x . loop (Assocs rho') body' $ viewABT body'
Nothing ->
-- TODO: even if we don't come up with a smarter way
-- of freshening variables, it'd be better to just pass
-- both sets to 'freshen' directly and then check them
-- each; rather than paying for taking their union every
-- time we go under a binder like this.
let x' = freshen x (fv0 `mappend` freeVars e) in
-- HACK: the 'rename' function requires an ABT not a
-- View, so we have to use 'caseBind' to give its
-- input and then 'viewABT' to discard the topmost
-- annotation. We really should find a way to eliminate
-- that overhead.
caseBind e $ \_x body' ->
bind x' . loop rho body' . viewABT $ rename x x' body'
-}
----------------------------------------------------------------
----------------------------------------------------------------
-- | A combinator for defining a HOAS-like API for our syntax.
-- Because our 'Term' is first-order, we cannot actually have any
-- exotic terms in our language. In principle, this function could
-- be used to do exotic things when constructing those non-exotic
-- terms; however, trying to do anything other than change the
-- variable's name hint will cause things to explode (since it'll
-- interfere with our tying-the-knot).
--
-- N.B., if you manually construct free variables and use them in
-- the body (i.e., via 'var'), they may become captured by the new
-- binding introduced here! This is inevitable since 'nextBind'
-- never looks at variable /use sites/; it only ever looks at
-- /binding sites/. On the other hand, if you manually construct a
-- bound variable (i.e., manually calling 'bind' yourself), then
-- the new binding introduced here will respect the old binding and
-- avoid that variable ID.
binder
:: (ABT syn abt)
=> Text -- ^ The variable's name hint
-> Sing a -- ^ The variable's type
-> (abt '[] a -> abt xs b) -- ^ Build the binder's body from a variable
-> abt (a ': xs) b
binder hint typ hoas = bind x body
where
body = hoas (var x)
x = Variable hint (nextBind body) typ
-- N.B., cannot use 'nextFree' when deciding the 'varID' of @x@
-- A Monadic variant of @binder@ which allows constructing a term in a monadic
-- context. The dependency on MonadFix is due to the knot-tying used to generate
-- the bound variable.
binderM
:: (MonadFix m, ABT syn abt)
=> Text
-> Sing a
-> (abt '[] a -> m (abt xs b))
-> m (abt (a ': xs) b)
binderM hint typ hoas = do
(var, body) <- mfix $ \ ~(_, b) -> do
let v = Variable hint (nextBind b) typ
b' <- hoas (var v)
return (v, b')
return (bind var body)
class (ABT syn abt) =>
Binders syn abt xs as | abt -> syn, abt xs -> as, abt as -> xs where
binders :: (as -> abt '[] b) -> abt xs b
instance (ABT syn abt) =>
Binders syn abt '[] () where
binders hoas = hoas ()
instance (Binders syn abt xs as, SingI x) =>
Binders syn abt (x ': xs) (abt '[] x, as) where
binders hoas = binder empty sing (binders . curry hoas)
{-
data Hint (a :: k)
= Hint !Text !(Sing a)
instance Show1 Hint where
showsPrec1 p (Hint x s) = showParen_01 p "Hint" x s
instance Show (Hint a) where
showsPrec = showsPrec1
show = show1
data VS (a :: k)
= VS {-# UNPACK #-} !Variable !(Sing a)
-- this typechecks, and it works!
-- BUG: but it seems fairly unusable. We must give explicit type signatures to any lambdas passed as the second argument, otherwise it complains about not knowing enough about the types in @xs@... Also, the uncurriedness of it isn't very HOAS-like
multibinder
:: (ABT abt) => List1 Hint xs -> (List1 abt xs -> abt b) -> abt b
multibinder names hoas = binds vars body
where
vars = go 0 names
where
-- BUG: this puts the largest binder on the inside
go :: Nat -> List1 Hint xs -> List1 VS xs
go _ Nil = Nil
go n (Cons (Hint name typ) rest) =
Cons (VS (Variable name (maxBind body + n) typ) typ)
((go $! n + 1) rest)
body = hoas (go vars)
where
go :: ABT abt => List1 VS xs -> List1 abt xs
go Nil = Nil
go (Cons (VS x typ) rest) = Cons (var x typ) (go rest)
binds :: ABT abt => List1 VS xs -> abt a -> abt a
binds Nil = id
binds (Cons (VS x _) rest) = bind x . binds rest
-}
----------------------------------------------------------------
----------------------------------------------------------------
-- TODO: versions of 'cataABT' and 'paraABT' which memoize the results for variables rather than recomputing them each time.
-- | The catamorphism (aka: iterator) for ABTs. While this is
-- equivalent to 'paraABT' in terms of the definable /functions/,
-- it is weaker in terms of definable /algorithms/. If you need
-- access to (subterms of) the original ABT, it is more efficient
-- to use 'paraABT' than to rebuild them. However, if you never
-- need access to the original ABT, then this function has somewhat
-- less overhead.
cataABT
:: forall
(abt :: [k] -> k -> *)
(syn :: ([k] -> k -> *) -> k -> *)
(r :: [k] -> k -> *)
. (ABT syn abt, Functor21 syn)
=> (forall a. Variable a -> r '[] a)
-> (forall x xs a. Variable x -> r xs a -> r (x ': xs) a)
-> (forall a. syn r a -> r '[] a)
-> forall xs a. abt xs a -> r xs a
cataABT var_ bind_ syn_ = start
where
start :: forall ys b. abt ys b -> r ys b
start = loop . viewABT
loop :: forall ys b. View (syn abt) ys b -> r ys b
loop (Syn t) = syn_ (fmap21 start t)
loop (Var x) = var_ x
loop (Bind x e) = bind_ x (loop e)
{-# INLINE cataABT #-}
-- | A monadic variant of @cataABT@, which may not fit the precise definition of
-- a catamorphism? The @bind@ and @syn@ operations receive monadic actions as their
-- inputs, which allows the @bind@ and @syn@ operations to update the monadic
-- context in which the subterms are evaluated if need be.
cataABTM
:: forall
(abt :: [k] -> k -> *)
(syn :: ([k] -> k -> *) -> k -> *)
(r :: [k] -> k -> *)
(f :: * -> *)
. (ABT syn abt, Traversable21 syn, Applicative f)
=> (forall a. Variable a -> f (r '[] a))
-> (forall x xs a. Variable x -> f (r xs a) -> f (r (x ': xs) a))
-> (forall a. f (syn r a) -> f (r '[] a))
-> forall xs a. abt xs a -> f (r xs a)
cataABTM var_ bind_ syn_ = start
where
start :: forall ys b. abt ys b -> f (r ys b)
start = loop . viewABT
loop :: forall ys b. View (syn abt) ys b -> f (r ys b)
loop (Syn t) = syn_ (traverse21 start t)
loop (Var x) = var_ x
loop (Bind x e) = bind_ x (loop e)
{-# INLINE cataABTM #-}
-- | The paramorphism (aka: recursor) for ABTs. While this is
-- equivalent to 'cataABT' in terms of the definable /functions/,
-- it is stronger in terms of definable /algorithms/. If you need
-- access to (subterms of) the original ABT, it is more efficient
-- to use this function than to use 'cataABT' and rebuild them.
-- However, if you never need access to the original ABT, then
-- 'cataABT' has somewhat less overhead.
--
-- The provided type is slightly non-uniform since we inline (i.e.,
-- curry) the definition of 'Pair2' in the type of the @bind_@
-- argument. But we can't inline 'Pair2' away in the type of the
-- @syn_@ argument. N.B., if you treat the second component of the
-- 'Pair2' (either the real ones or the curried ones) lazily, then
-- this is a top-down function; however, if you treat them strictly
-- then it becomes a bottom-up function.
paraABT
:: forall
(abt :: [k] -> k -> *)
(syn :: ([k] -> k -> *) -> k -> *)
(r :: [k] -> k -> *)
. (ABT syn abt, Functor21 syn)
=> (forall a. Variable a -> r '[] a)
-> (forall x xs a. Variable x -> abt xs a -> r xs a -> r (x ': xs) a)
-> (forall a. syn (Pair2 abt r) a -> r '[] a)
-> forall xs a. abt xs a -> r xs a
paraABT var_ bind_ syn_ = start
where
start :: forall ys b. abt ys b -> r ys b
start = loop . viewABT
loop :: forall ys b. View (syn abt) ys b -> r ys b
loop (Syn t) = syn_ (fmap21 (\e -> Pair2 e (start e)) t)
loop (Var x) = var_ x
loop (Bind x e) = bind_ x (unviewABT e) (loop e)
-- HACK: how can we avoid that call to 'unviewABT'?
{-# INLINE paraABT #-}
----------------------------------------------------------------
----------------------------------------------------------------
-- TODO: Swap the argument order?
-- | If the expression is a variable, then look it up. Recursing
-- until we can finally return some syntax.
resolveVar
:: (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), ABT syn abt)
=> abt '[] (a :: k)
-> Assocs (abt '[])
-> Either (Variable a) (syn abt a)
resolveVar e xs =
flip (caseVarSyn e) Right $ \x ->
case lookupAssoc x xs of
Just e' -> resolveVar e' xs
Nothing -> Left x
----------------------------------------------------------------
----------------------------------------------------------- fin.