Representation & Evaluation of Typed Expressions

Date
Tags coco, programming, research
Target Audience Haskell programmers.
Epistemic Status I wrote this memo to work out how to implement CoCo. So this all works and is, mostly, still implemented like this.

Or, “I tried really hard to use the bound lib­rary but just couldn’t get that square peg in this round hole.”

This is a sim­pli­fied ver­sion of a problem I’ve been having in CoCo. The cur­rent hand­ling of vari­ables in CoCo is very poor, the pro­grammer has to spe­cify ex­actly which vari­ables may be in­tro­duced, binds and lets cause shad­ow­ing, and no care is taken to avoid gen­er­ating alpha equi­valent terms.

Here are two rep­res­ent­ative prob­lems:

  1. If you have the vari­able x, and no oth­ers, a term like this will not be gen­er­ated: f >>= \x1 -> g x1 x

  2. If you have the vari­ables x and y of the same type, these equi­valent terms will be gen­er­ated: f x and f y

Let’s get star­ted…

{-# LAN­GUAGE Kind­Sig­na­tures #-}
{-# LAN­GUAGE Scoped­TypeVari­ables #-}

im­port Data.­Dy­namic (Dy­namic, dyn­Apply, dyn­Ty­peRep)
im­port Data.­Func­tion (on)
im­port Data.List (groupBy, nub, sortOn)
im­port Data.Maybe (map­Maybe, may­beToList)
im­port Data.Ord (Down(..))
im­port Data.­Proxy (Proxy(..))
im­port Data.­Type­able (Type­able, Ty­peRep, fun­Res­ultTy, splitTy­ConApp, typeOf, ty­peRep)
im­port Data.­Void (Void, ab­surd)
im­port GH­C.Exts (Any)
im­port Un­safe.­Co­erce (un­sa­fe­Co­erce)

Mark 1: A Simple Typed Ex­pres­sion Type

Our ex­pres­sions are rep­res­ent­a­tions of Haskell code, which makes this a bit un­like most toy ex­pres­sion eval­u­ators you see in tu­tori­als. We want everything to be very typed, and not ex­pose the con­structors of the ex­pres­sion data type, using smart con­structors to en­sure that only well-­typed ex­pres­sions can be cre­ated.

It’s this typing that makes it really dif­fi­cult to use the bound lib­rary here, as bound doesn’t play so nicely with typed vari­ables. You can infer types for vari­ables later, but I don’t really want to im­ple­ment that.

-- | A type for ex­pres­sions. This would not be ex­ported by ac­tual lib­rary code, to pre­vent the user
-- from mucking around with the types.
data Exp1
  = Lit1 String Dy­namic
  -- ^ Lit­eral values are just dy­nam­ic­ally-wrapped Haskell val­ues.
  | Hole1 Ty­peRep
  -- ^ "Holes" are free vari­ables, iden­ti­fied by their po­s­i­tion in the tree.
  | Named1 Ty­peRep String
  -- ^ Vari­ables which are bound by a provided en­vir­on­ment. More on this later.
  | Bound1 Ty­peRep Int
  -- ^ Vari­ables which are bound by a let, with de Bruijn in­dices. All vari­ables bound to the same
  -- let must have the cor­rect type.
  | Let1 Ty­peRep Exp1 Exp1
  -- ^ The binder is as­sumed to be of the cor­rect type for all the vari­ables bound to it.
  | Ap1 Ty­peRep Exp1 Exp1
  -- ^ The para­meter is as­sumed to be of the cor­rect type for the func­tion.

in­stance Show Exp1 where
  show (Lit1 s _) = s
  show (Hole1 ty) = "(_ :: " ++ show ty ++ ")"
  show (Named1 ty s) = "(" ++ s ++ " :: " ++ show ty ++ ")"
  show (Bound1 ty i) = "(" ++ show i ++ " :: " ++ show ty ++ ")"
  show (Let1 _ b e) = "let <" ++ show b ++ "> in <" ++ show e ++ ">"
  show (Ap1  _ f e) = "(" ++ show f ++ ") (" ++ show e ++ ")"

-- | Get the type of an ex­pres­sion.
typeOf1 :: Exp1 -> Ty­peRep
typeOf1 (Lit1 _ dyn)  = dyn­Ty­peRep dyn
typeOf1 (Hole1  ty)   = ty
typeOf1 (Named1 ty _) = ty
typeOf1 (Bound1 ty _) = ty
typeOf1 (Let1 ty _ _) = ty
typeOf1 (Ap1  ty _ _) = ty

-- | Get all the holes in an ex­pres­sion, iden­ti­fied by po­s­i­tion.
holes1 :: Exp1 -> [(Int, Ty­peRep)]
holes1 = fst . go 0 where
  go i (Hole1 ty) = ([(i, ty)], i + 1)
  go i (Let1 _ b e) =
    let (bhs, i')  = go i  b
        (ehs, i'') = go i' e
    in (bhs ++ ehs, i'')
  go i (Ap1 _ f e) =
    let (fhs, i')  = go i  f
        (ehs, i'') = go i' e
    in (fhs ++ ehs, i'')
  go i _ = ([], i)

-- | Get all the named vari­ables in an ex­pres­sion.
names1 :: Exp1 -> [(String, Ty­peRep)]
names1 = nub . go where
  go (Named1 ty s) = [(s, ty)]
  go (Let1 _ b e) = go b ++ go e
  go (Ap1 _ f e) = go f ++ go e
  go _ = []

Smart con­structors: we only want to be able to pro­duce type-­cor­rect ex­pres­sions, for two reas­ons: the eval­u­ator in CoCo is more com­plex and does a lot of un­safe co­er­cion, and being able to just call error when the types don’t work out is nicer than needing to ac­tu­ally handle it; and it makes it easier to gen­erate terms pro­gram­mat­ic­ally, as you simply try all pos­sib­il­ities and keep the ones which suc­ceed.

-- | Con­struct a lit­eral value.
lit1 :: String -> Dy­namic -> Exp1
lit1 = Lit1

-- | Con­struct a typed hole.
hole1 :: Ty­peRep -> Exp1
hole1 = Hole1

-- | Per­form a func­tion ap­plic­a­tion, if type-­cor­rect.
ap1 :: Exp1 -> Exp1 -> Maybe Exp1
ap1 f e = (\ty -> Ap1 ty f e) <$> typeOf1 f `fun­Res­ultTy` typeOf1 e

-- | Bind a col­lec­tion of holes, if type-­cor­rect.
--
-- The binding is ap­plied "atom­ic­ally", in that you don't need to worry about holes dis­ap­pearing and
-- so chan­ging their po­s­i­tion-in­dices while this op­er­a­tion hap­pens; how­ever the po­s­i­tion of un­bound
-- holes may be altered in the result of this func­tion.
let1 :: [Int] -> Exp1 -> Exp1 -> Maybe Exp1
let1 is b e0 = Let1 (typeOf1 e0) b . fst <$> go 0 0 e0 where
  go n i (Hole1 ty)
    | i `elem` is = if typeOf1 b == ty then Just (Bound1 ty n, i + 1) else Nothing
    | oth­er­wise   = Just (Hole1 ty, i + 1)
  go n i (Let1 ty b e) = do
    (b', i')  <- go n     i  b
    (e', i'') <- go (n+1) i' e
    Just (Let1 ty b' e', i'')
  go n i (Ap1 ty f e) = do
    (f', i')  <- go n i  f
    (e', i'') <- go n i' e
    Just (Ap1 ty f' e', i'')
  go _ i e = Just (e, i)

-- | Give names to holes, if type-­cor­rect.
--
-- This has the same in­dexing be­ha­viour as 'let1'.
name1 :: [(Int, String)] -> Exp1 -> Maybe Exp1
name1 is e0 = (\(e,_,_) -> e) <$> go [] 0 e0 where
  go env i n@(Named1 ty s) = case lookup s env of
    -- if a name gets re-used it had better be at the same type!
    Just sty
      | ty == sty -> Just (n, env, i)
      | oth­er­wise -> Nothing
    Nothing -> Just (n, env, i)
  go env i (Hole1 ty) = case lookup i is of
    Just s -> case lookup s env of
      Just sty
        | ty == sty -> Just (Named1 ty s, env, i + 1)
        | oth­er­wise -> Nothing
      Nothing -> Just (Named1 ty s, (s,ty):env, i + 1)
    Nothing -> Just (Hole1 ty, env, i + 1)
  go env i (Let1 ty b e) = do
    (b', env',  i')  <- go env  i  b
    (e', env'', i'') <- go env' i' e
    Just (Let1 ty b' e', env'', i'')
  go env i (Ap1 ty f e) = do
    (f', env',  i')  <- go env  i  f
    (e', env'', i'') <- go env' i' e
    Just (Ap1 ty f' e', env'', i'')
  go env i e = Just (e, env, i)

Eval­u­ation: now we have everything in place to eval­uate ex­pres­sions with no un­bound holes. Everything is type-­cor­rect-by-­con­struc­tion, so if there are no holes (and the global en­vir­on­ment has everything we need) we can get out a value.

-- | Eval­uate an ex­pres­sion if it has no holes.
eval1 :: [(String, Dy­namic)] -> Exp1 -> Maybe Dy­namic
eval1 globals = go [] where
  -- the local en­vir­on­ment is a list of val­ues, with each new scope pre­pending a value; this means
  -- that the de Bruijn in­dices cor­res­pond with list in­dices
  go locals (Let1 _ b e) = (\dyn -> go (dyn:locals) e) =<< go locals b
  go locals (Bound1 _ n) = Just (locals !! n)
  -- named vari­ables come from the global en­vir­on­ment
  go _ (Named1 ty s) = case lookup s globals of
    Just dyn | dyn­Ty­peRep dyn == ty -> Just dyn
    _ -> Nothing
  -- the other op­er­a­tions don't care about either en­vir­on­ment
  go locals (Ap1 _ f e) = do
    dynf <- go locals f
    dyne <- go locals e
    dynf `dyn­Apply` dyne
  go _ (Lit1 _ dyn) = Just dyn
  go _ (Hole1 _)  = Nothing

Re­moving Holes: we still have one more prob­lem, it would be nice for holes to be given names auto­mat­ic­ally, and not just in­di­vidual holes, but groups of holes too.

For ex­ample, if we have an ex­pres­sion like so:

f (_ :: Int) (_ :: Bool) (_ :: Bool) (_ :: Int)

It would be nice to be able to gen­erate these ex­pres­sions auto­mat­ic­ally:

f (w :: Int) (x :: Bool) (y :: Bool) (z :: Int)
f (w :: Int) (x :: Bool) (y :: Bool) (w :: Int)
f (w :: Int) (x :: Bool) (x :: Bool) (z :: Int)
f (w :: Int) (x :: Bool) (x :: Bool) (w :: Int)

It would be par­tic­u­larly nice if they were gen­er­ated in a list in that or­der, from most free to most con­strained.

-- | From an ex­pres­sion that may have holes, gen­erate a list of ex­pres­sions with named vari­ables
-- sub­sti­tuted in­stead, ordered from most free (one hole per vari­able) to most con­strained (mul­tiple
-- holes per vari­able).
--
-- This takes a func­tion to as­sign a letter to each type, sub­sequent vari­ables of the same type have
-- di­gits ap­pen­ded.
terms1 :: (Ty­peRep -> Char) -> Exp1 -> [Exp1]
terms1 nf = sortOn (Down . length . names1) . go where
  go e0 = case hs e0 of
    [] -> [e0]
    (chosen:_) -> con­catMap go
      [ e | ps <- par­ti­tions chosen
          , let (((_,tyc):_):_) = ps
          , let vname i = if i == 0 then [nf tyc] else nf tyc : show i
          , let naming = concat $ zip­With (\i vs -> [(v, vname i) | (v,_) <- vs]) [0..] ps
          , e <- may­beToList (name1 naming e0)
      ]

  -- holes grouped by type
  hs = groupBy ((==) `on` snd) . sortOn snd . holes1

  -- all par­ti­tions of a list
  par­ti­tions (x:xs) =
    [[x]:p | p <- par­ti­tions xs] ++
    [(x:ys):yss | (ys:yss) <- par­ti­tions xs]
  par­ti­tions [] = [[]]

Here’s an ex­ample from ghci:

λ> let in­tHole  = hole1 $ T.­typeOf (5::Int)
λ> let bool­Hole = hole1 $ T.­typeOf True
λ> let ibf      = lit1 "f" (D.toDyn ((\_ _ _ a -> a) :: Int -> Bool -> Bool -> Int -> Int))
λ> let ib­fExp   = fromJust $ do { x <- ibf `ap1` in­tHole; y <- x `ap1` bool­Hole; z <- y `ap1` bool­Hole; z `ap1` in­tHole }
λ> mapM_ print $ terms1 (head.show) ib­fExp
((((f) ((I :: In­t))) ((B :: Bool))) ((B1 :: Bool))) ((I1 :: Int))
((((f) ((I :: In­t))) ((B :: Bool))) ((B1 :: Bool))) ((I :: Int))
((((f) ((I :: In­t))) ((B :: Bool))) ((B :: Bool))) ((I1 :: Int))
((((f) ((I :: In­t))) ((B :: Bool))) ((B :: Bool))) ((I :: Int))

Pretty sweet!

Mark 2: More Type Safety

What we have now is pretty good, but it leaves a little to be de­sired: it would be nice to be able to stat­ic­ally forbid passing ex­pres­sions with holes to eval. As al­ways in Haskell, the solu­tion is to add an­other type para­meter.

data Exp2 h
  = Lit2 String Dy­namic
  | Var2 Ty­peRep (Var2 h)
  -- ^ One con­structor for holes, named, and bound vari­ables.
  | Let2 Ty­peRep (Exp2 h) (Exp2 h)
  | Ap2  Ty­peRep (Exp2 h) (Exp2 h)

in­stance Show (Exp2 h) where
  show (Lit2 s _) = s
  show (Var2 ty v) = "(" ++ show v ++ " :: " ++ show ty ++ ")"
  show (Let2 _ b e) = "let <" ++ show b ++ "> in <" ++ show e ++ ">"
  show (Ap2 _ f e)  = "(" ++ show f ++ ") (" ++ show e ++ ")"

data Var2 h
  = Hole2 h
  -- ^ Holes get a typed tag.
  | Named2 String
  -- ^ En­vir­on­ment vari­ables.
  | Bound2 Int
  -- ^ Let-bound vari­ables.

in­stance Show (Var2 h) where
  show (Hole2  _) = "_"
  show (Named2 s) = s
  show (Bound2 i) = show i

Schemas and Terms: what does this hole tag buy us? Well, ac­tu­ally, it lets us very simply forbid the pres­ence of holes! Con­structing an h value is re­quired to con­struct a hole, so if we set it to Void, then no holes can be made at all! If the tag is some in­hab­ited type, then an ex­pres­sion may con­tain holes (but may not).

Let’s in­tro­duce two type syn­onyms to talk about these:

-- | A schema is an ex­pres­sion which may con­tain holes. A single schema may cor­res­pond to many
-- terms.
type Schema2 = Exp2 ()

-- | A term is an ex­pres­sion with no holes. Many terms may cor­res­pond to a single schema.
type Term2 = Exp2 Void

-- | Con­vert a Schema into a Term if there are no holes.
toTerm2 :: Schema2 -> Maybe Term2
toTerm2 (Lit2 s dyn) = Just (Lit2 s dyn)
toTerm2 (Var2 ty v) = case v of
  Hole2  _ -> Nothing
  Named2 s -> Just (Var2 ty (Named2 s))
  Bound2 i -> Just (Var2 ty (Bound2 i))
toTerm2 (Let2 ty b e) = Let2 ty <$> toTerm2 b <*> toTerm2 e
toTerm2 (Ap2  ty f e) = Ap2  ty <$> toTerm2 f <*> toTerm2 e

Eval­u­ation & Hole Re­moval: now we can eval­uate terms after re­moving holes from schemas. Stat­ic­ally-checked guar­an­tees that we’re dealing with all of our holes prop­erly, nice!

-- | Eval­uate a term
eval2 :: [(String, Dy­namic)] -> Term2 -> Maybe Dy­namic
eval2 globals = go [] where
  go locals (Let2 _ b e) = (\dyn -> go (dyn:locals) e) =<< go locals b
  go locals v@(Var2 _ _) = env locals v
  go locals (Ap2 _ f e) = do
    dynf <- go locals f
    dyne <- go locals e
    dynf `dyn­Apply` dyne
  go _ (Lit2 _ dyn) = Just dyn

  env locals (Var2 _ (Bound2 n))
    | length locals > n = Just (locals !! n)
    | oth­er­wise = Nothing
  env _ (Var2 ty (Named2 s)) = case lookup s globals of
    Just dyn | dyn­Ty­peRep dyn == ty -> Just dyn
    _ -> Nothing
  env _ (Var2 _ (Hole2 v)) = ab­surd v -- this is ac­tu­ally un­reach­able now

-- | From a schema that may have holes, gen­erate a list of terms with named vari­ables
-- sub­sti­tuted in­stead.
terms2 :: (Ty­peRep -> Char) -> Schema2 -> [Term2]
terms2 nf = map­Maybe toTerm2 . sortOn (Down . length . names2) . go where
  go e0 = case hs e0 of
    [] -> [e0]
    (chosen:_) -> con­catMap go
      [ e | ps <- par­ti­tions chosen
          , let (((_,tyc):_):_) = ps
          , let vname i = if i == 0 then [nf tyc] else nf tyc : show i
          , let naming = concat $ zip­With (\i vs -> [(v, vname i) | (v,_) <- vs]) [0..] ps
          , e <- may­beToList (name2 naming e0)
      ]

  -- holes grouped by type
  hs = groupBy ((==) `on` snd) . sortOn snd . holes2

  -- all par­ti­tions of a list
  par­ti­tions (x:xs) =
    [[x]:p | p <- par­ti­tions xs] ++
    [(x:ys):yss | (ys:yss) <- par­ti­tions xs]
  par­ti­tions [] = [[]]

The rest of the code hasn’t changed much, but is in­cluded for com­plete­ness:

-- | Get the type of an ex­pres­sion.
typeOf2 :: Exp2 h -> Ty­peRep
typeOf2 (Lit2 _ dyn)  = dyn­Ty­peRep dyn
typeOf2 (Var2 ty _)   = ty
typeOf2 (Let2 ty _ _) = ty
typeOf2 (Ap2  ty _ _) = ty

-- | Get all the holes in an ex­pres­sion, iden­ti­fied by po­s­i­tion.
holes2 :: Schema2 -> [(Int, Ty­peRep)]
holes2 = fst . go 0 where
  go i (Var2 ty (Hole2 _)) = ([(i, ty)], i + 1) -- tag is ig­nored
  go i (Let2 _ b e) =
    let (bhs, i')  = go i  b
        (ehs, i'') = go i' e
    in (bhs ++ ehs, i'')
  go i (Ap2 _ f e) =
    let (fhs, i')  = go i  f
        (ehs, i'') = go i' e
    in (fhs ++ ehs, i'')
  go i _ = ([], i)

-- | Get all the named vari­ables in an ex­pres­sion.
names2 :: Exp2 h -> [(String, Ty­peRep)]
names2 = nub . go where
  go (Var2 ty (Named2 s)) = [(s, ty)]
  go (Let2 _ b e) = go b ++ go e
  go (Ap2 _ f e) = go f ++ go e
  go _ = []

-- | Con­struct a lit­eral value.
lit2 :: String -> Dy­namic -> Exp2 h
lit2 = Lit2

-- | Con­struct a typed hole.
hole2 :: Ty­peRep -> Schema2
hole2 ty = Var2 ty (Hole2 ()) -- holes get tagged with unit

-- | Per­form a func­tion ap­plic­a­tion, if type-­cor­rect.
ap2 :: Exp2 h -> Exp2 h -> Maybe (Exp2 h)
ap2 f e = (\ty -> Ap2 ty f e) <$> typeOf2 f `fun­Res­ultTy` typeOf2 e

-- | Bind a col­lec­tion of holes, if type-­cor­rect.
let2 :: [Int] -> Schema2 -> Schema2 -> Maybe Schema2
let2 is b e0 = Let2 (typeOf2 e0) b . fst <$> go 0 0 e0 where
  go n i (Var2 ty (Hole2 h))
    | i `elem` is = if typeOf2 b == ty then Just (Var2 ty (Bound2 n), i + 1) else Nothing -- tag is ig­nored
    | oth­er­wise   = Just (Var2 ty (Hole2 h), i + 1) -- tag is pre­served
  go n i (Let2 ty b e) = do
    (b', i')  <- go n     i  b
    (e', i'') <- go (n+1) i' e
    Just (Let2 ty b' e', i'')
  go n i (Ap2 ty f e) = do
    (f', i')  <- go n i  f
    (e', i'') <- go n i' e
    Just (Ap2 ty f' e', i'')
  go _ i e = Just (e, i)

-- | Give names to holes, if type-­cor­rect.
name2 :: [(Int, String)] -> Schema2 -> Maybe Schema2
name2 is e0 = (\(e,_,_) -> e) <$> go [] 0 e0 where
  go env i n@(Var2 ty (Named2 s)) = case lookup s env of
    Just sty
      | ty == sty -> Just (n, env, i)
      | oth­er­wise -> Nothing
    Nothing -> Just (n, env, i)
  go env i (Var2 ty (Hole2 h)) = case lookup i is of
    Just s -> case lookup s env of
      Just sty
        | ty == sty -> Just (Var2 ty (Named2 s), env, i + 1) -- tag is ig­nored
        | oth­er­wise -> Nothing
      Nothing -> Just (Var2 ty (Named2 s), (s,ty):env, i + 1) -- tag is ig­nored
    Nothing -> Just (Var2 ty (Hole2 h), env, i + 1) -- tag is pre­served
  go env i (Let2 ty b e) = do
    (b', env',  i')  <- go env  i  b
    (e', env'', i'') <- go env' i' e
    Just (Let2 ty b' e', env'', i'')
  go env i (Ap2 ty f e) = do
    (f', env',  i')  <- go env  i  f
    (e', env'', i'') <- go env' i' e
    Just (Ap2 ty f' e', env'', i'')
  go env i e = Just (e, env, i)

Aside: The Im­ple­ment­a­tion of Data.­Dy­namic

In the Mark 3 eval­u­ator, we’re going to need a func­tion of type Monad m => m Dy­namic -> Dy­namic, which “pushes” the m in­side the Dy­namic, and of type Monad m => Dy­namic -> Maybe (m Dy­namic). Un­for­tu­nately, Data.­Dy­namic doesn’t provide a way to do this, for good reason: it’s im­possible in gen­eral! There’s no way to know what the type of the dy­namic value in­side the monad is, so there’s no way to do this safely.

For­tu­nately, im­ple­menting a Data.­Dy­nam­ic-lite is pretty simple.

-- | A dy­namic value is a pair of its type and 'Any'. Any is a ma­gical type which is guar­an­teed to
-- | work with 'un­sa­fe­Co­er­ce'.
data BDy­namic = BDy­namic { bdyn­Ty­peRep :: Ty­peRep, bdynAny :: Any }

in­stance Show BDy­namic where
  show = show . bdyn­Ty­peRep

(BDy­namic for “bar­ru­cadu’s dy­nam­ic”)

We need to be able to con­struct and de­con­struct dy­namic val­ues, these op­er­a­tions do use un­sa­fe­Co­erce, but are safe:

-- | Con­vert an ar­bit­rary value into a dy­namic one.
toB­Dy­namic :: Type­able a => a -> BDy­namic
toB­Dy­namic a = BDy­namic (typeOf a) (un­sa­fe­Co­erce a)

-- | Con­vert a dy­namic value into an or­dinary value, if the types match.
fromBDy­namic :: Type­able a => BDy­namic -> Maybe a
fromBDy­namic (BDy­namic ty v) = case un­sa­fe­Co­erce v of
  -- this is a bit mind-bend­ing, but the 'typeOf r' here is the type of the 'a', as 'un­sa­fe­Co­erce
  -- v :: a' (regard­less of whether it ac­tu­ally is an 'a' value or not). The same result could be
  -- achieved using Scoped­TypeVari­ables and 'ty­peR­ep'.
  r | ty == typeOf r -> Just r
    | oth­er­wise      -> Nothing

The final op­er­a­tion needed for the Marks 1 and 2 im­ple­ment­a­tion is func­tion ap­plic­a­tion:

-- | Dy­nam­ic­ally-­typed func­tion ap­plic­a­tion.
bdyn­Apply :: BDy­namic -> BDy­namic -> Maybe BDy­namic
bdyn­Apply (BDy­namic ty1 f) (BDy­namic ty2 x) = case fun­Res­ultTy ty1 ty2 of
  Just ty3 -> Just (BDy­namic ty3 ((un­sa­fe­Co­erce f) x))
  Nothing  -> Nothing

Now we can con­struct our strange mon­ad-shuff­ling op­er­a­tions:

-- | "Push" a functor in­side a dy­namic value, given the type of the res­ultant value.
--
-- This is un­safe be­cause if the type is in­cor­rect and the value is later used as that type, good
-- luck.
un­safe­Wrap­Functor :: Functor f => Ty­peRep -> f BDy­namic -> BDy­namic
un­safe­Wrap­Functor ty fdyn = BDy­namic ty (un­sa­fe­Co­erce $ fmap bdynAny fdyn)

-- | "Ex­tract" a functor from a dy­namic value.
un­wrap­Functor :: forall f. (Functor f, Type­able f) => BDy­namic -> Maybe (f BDy­namic)
un­wrap­Functor (BDy­namic ty v) = case splitTy­ConApp ty of
    (tyCon, tyArgs)
      | tyCon == ftyCon && not (null tyArgs) && init tyArgs == ft­yArgs
        -> Just $ BDy­namic (last tyArgs) <$> un­sa­fe­Co­erce v
    _ -> Nothing
  where
    (ftyCon, ft­yArgs) = splitTy­ConApp (ty­peRep (Proxy :: Proxy f))

It’s al­most a shame that Data.­Dy­namic doesn’t ex­pose enough to im­ple­ment this. It has gone for a safe but lim­ited API. A common Haskell “design” pat­tern is to have safe public APIs and un­safe but pub­lic­ally-­ex­posed “in­ternal” APIs, but base doesn’t seem to follow that.

Mark 3: Mon­adic Ex­pres­sions

This ex­pres­sion rep­res­ent­a­tion is pretty nice, but it’s rather cum­ber­some to ex­press mon­adic op­er­a­tions for a couple of reas­ons:

  1. Everything is mono­morphic, so there would need to be a sep­arate lit for >>= at every de­sired type.

  2. Due to func­tion ap­plic­a­tion having a Maybe res­ult, even at a single type writing ap2 (lit2 ((>>=) :: Type)) e1 >>= \f -> ap2 f e2 is not nice.

  3. The ori­ginal need for this ex­pres­sion rep­res­ent­a­tion was for gen­er­ating Haskell terms, and gen­er­ating lambda terms is tricky; it would be nice to be able to bind holes dir­ectly.

This calls for a third rep­res­ent­a­tion of ex­pres­sions. For reasons that will be­come ap­parent when looking at the eval­u­ator, we’ll specalise this to only working in one monad, and track the monad type as an­other para­meter of Exp:

data Exp3 (m :: * -> *) (h :: *)
  = Lit3 String BDy­namic
  | Var3 Ty­peRep (Var3 h)
  | Bind3 Ty­peRep (Exp3 m h) (Exp3 m h)
  | Let3  Ty­peRep (Exp3 m h) (Exp3 m h)
  | Ap3   Ty­peRep (Exp3 m h) (Exp3 m h)

in­stance Show (Exp3 m h) where
  show (Lit3 s _) = s
  show (Var3 ty v) = "(" ++ show v ++ " :: " ++ show ty ++ ")"
  show (Bind3 _ b e) = "bind <" ++ show b ++ "> in <" ++ show e ++ ">"
  show (Let3  _ b e) = "let <" ++ show b ++ "> in <" ++ show e ++ ">"
  show (Ap3   _ f e) = "(" ++ show f ++ ") (" ++ show e ++ ")"

Con­struc­tion: bind is going to be treated just as a let with spe­cial eval­u­ation rules. This means that de Bruijn in­dices will be able to refer to a bind or a let. Rather than have two sep­arate coun­ters for those, we’ll just put everything in the same namespace (in­dex-space?).

-- | Bind a col­lec­tion of holes, if type-­cor­rect.
let3 :: [Int] -> Schema3 m -> Schema3 m -> Maybe (Schema3 m)
let3 is b e0 = Let3 (typeOf3 e0) b <$> let­Or­B­ind3 is (typeOf3 b) e0

-- | Mon­ad­ic­ally bind a col­lec­tion of holes, if type-­cor­rect.
--
-- This has the same in­dexing be­ha­viour as 'let3'.
bind3 :: forall m. Type­able m => [Int] -> Schema3 m -> Schema3 m -> Maybe (Schema3 m)
bind3 is b e0 = case (splitTy­ConApp (typeOf3 b), splitTy­ConApp (typeOf3 e0)) of
    ((btyCon, bt­yArgs), (etyCon, et­yArgs))
      | btyCon == mtyCon && btyCon == etyCon && not (null bt­yArgs) && not (null et­yArgs) && mt­yArgs == init bt­yArgs && init bt­yArgs == init et­yArgs
        -> Bind3 (typeOf3 e0) b <$> let­Or­B­ind3 is (last bt­yArgs) e0
    _ -> Nothing
  where
    (mtyCon, mt­yArgs) = splitTy­ConApp (ty­peRep (Proxy :: Proxy m))

-- | A helper for 'bind3' and 'let3': bind holes to the top of the ex­pres­sion.
let­Or­B­ind3 :: [Int] -> Ty­peRep -> Exp3 m h -> Maybe (Exp3 m h)
let­Or­B­ind3 is boundTy e0 = fst <$> go 0 0 e0 where
  go n i (Var3 ty (Hole3 h))
    | i `elem` is = if boundTy == ty then Just (Var3 ty (Bound3 n), i + 1) else Nothing
    | oth­er­wise   = Just (Var3 ty (Hole3 h), i + 1)
  go n i (Bind3 ty b e) = do -- a new case for Bind3, the same as the case for Let3
    (b', i')  <- go n     i  b
    (e', i'') <- go (n+1) i' e
    Just (Bind3 ty b' e', i'')
  go n i (Let3 ty b e) = do
    (b', i')  <- go n     i  b
    (e', i'') <- go (n+1) i' e
    Just (Let3 ty b' e', i'')
  go n i (Ap3 ty f e) = do
    (f', i')  <- go n i  f
    (e', i'') <- go n i' e
    Just (Ap3 ty f' e', i'')
  go _ i e = Just (e, i)

We could make let­Or­B­ind3 also work for name3 by car­rying around a third state token and let­ting the Var3 case apply an ar­bit­rary func­tion.

Eval­u­ation: the new bind case, un­for­tu­nately, com­plic­ates things some­what here. It’s much more awk­ward to deal with er­rors during eval­u­ation, but for­tu­nately the only er­rors that can ac­tu­ally arise are un­bound named vari­ables: the smart con­structors en­sure ex­pres­sions are well-­typed and have valid de Bruijn in­dices. This means we can just check the named vari­ables for validity up front and then use error once we’re sure there ac­tu­ally are no er­rors.

-- | Eval­uate a term
eval3 :: forall m. (Monad m, Type­able m) => [(String, BDy­namic)] -> Term3 m -> Maybe BDy­namic
eval3 globals e0
    | all check (names3 e0) = Just (go [] e0)
    | oth­er­wise = Nothing
  where
    go locals (Bind3 ty b e) = case (un­wrap­Functor :: BDy­namic -> Maybe (m BDy­namic)) (go locals b) of
      Just mdyn -> un­safe­Wrap­Functor ty $ mdyn >>= \dyn -> case un­wrap­Functor (go (dyn:locals) e) of
        Just dyn -> dyn
        Nothing -> error "type error I can't deal with here!" -- this is un­reach­able
      Nothing -> error "type error I can't deal with here!" -- this is un­reach­able
    go locals (Let3 _ b e) = go (go locals b : locals) e
    go locals v@(Var3 _ _) = case env locals v of
      Just dyn -> dyn
      Nothing -> error "en­vir­on­ment error I can't deal with here!" -- this is un­reach­able
    go locals (Ap3 _ f e) = case go locals f `bdyn­Apply` go locals e of
      Just dyn -> dyn
      Nothing -> error "type error I can't deal with here!" -- this is un­reach­able
    go _ (Lit3 _ dyn) = dyn

    env locals (Var3 _ (Bound3 n))
      | length locals > n = Just (locals !! n)
      | oth­er­wise = Nothing
    env _ (Var3 ty (Named3 s)) = case lookup s globals of
      Just dyn | bdyn­Ty­peRep dyn == ty -> Just dyn
      _ -> Nothing
    env _ (Var3 _ (Hole3 v)) = ab­surd v

    check (s, ty) = case lookup s globals of
      Just dyn -> bdyn­Ty­peRep dyn == ty
      Nothing  -> False

Now it be­comes ap­parent why the monad type para­meter is needed in the ex­pres­sion type, the eval­u­ator uses >>=, and so it needs to know which monad to bind it as. An al­tern­ative would be to use a type like this, but this still re­stricts you to using a single monad and so doesn’t gain any­thing:

eval­3alt :: (Monad m, Type­able m) => proxy m -> [(String, BDy­nam­ic)] -> Term3 -> Maybe BDy­namic

Here’s a little ex­ample showing that side-ef­fects do work (when I first did this, they did­n’t, so it’s not quite trivial to get right):

λ> r <- newIORef (5::Int)
λ> let in­tHole = hole3 $ T.­typeOf (5::Int)
λ> let plusLit = lit3 "+" . toB­Dy­namic $ ((+) :: Int -> Int -> Int)
λ> let plusTwo = fromJust $ (fromJust $ plusLit `ap3` in­tHole) `ap3` in­tHole
λ> let pureInt = lit3 "pure" . toB­Dy­namic $ (pure :: Int -> IO Int)
λ> let plusT­woIO = fromJust $ pureInt `ap3` plusTwo
λ> let in­t­And­Times = (lit3 "*2" . toB­Dy­namic $ (modi­fyIORef r (*7) >> pure (7::Int))) :: Exp3 IO h
λ> let eval = fromJust $ (fromBDy­namic :: BDy­namic -> Maybe (IO Int)) =<< eval3 [] =<< toTerm3 =<< bind3 [0,1] in­t­And­Times plusT­woIO
λ> eval
14
λ> readIORef r
7
λ> eval
14
λ> readIORef r
49

Again, the rest of the code hasn’t changed much, but is in­cluded for com­plete­ness.

data Var3 h
  = Hole3  h
  | Named3 String
  | Bound3 Int

in­stance Show (Var3 h) where
  show (Hole3  _) = "_"
  show (Named3 s) = s
  show (Bound3 i) = show i

-- | A schema is an ex­pres­sion which may con­tain holes.
type Schema3 m = Exp3 m ()

-- | A term is an ex­pres­sion with no holes.
type Term3 m = Exp3 m Void

-- | Con­vert a Schema into a Term if there are no holes.
toTerm3 :: Schema3 m -> Maybe (Term3 m)
toTerm3 (Lit3 s dyn) = Just (Lit3 s dyn)
toTerm3 (Var3 ty v) = case v of
  Hole3  _ -> Nothing
  Named3 s -> Just (Var3 ty (Named3 s))
  Bound3 i -> Just (Var3 ty (Bound3 i))
toTerm3 (Bind3 ty b e) = Bind3 ty <$> toTerm3 b <*> toTerm3 e
toTerm3 (Let3  ty b e) = Let3  ty <$> toTerm3 b <*> toTerm3 e
toTerm3 (Ap3   ty f e) = Ap3   ty <$> toTerm3 f <*> toTerm3 e

-- | Get the type of an ex­pres­sion.
typeOf3 :: Exp3 m h -> Ty­peRep
typeOf3 (Lit3  _ dyn)  = bdyn­Ty­peRep dyn
typeOf3 (Var3  ty _)   = ty
typeOf3 (Bind3 ty _ _) = ty
typeOf3 (Let3  ty _ _) = ty
typeOf3 (Ap3   ty _ _) = ty

-- | Get all the holes in an ex­pres­sion, iden­ti­fied by po­s­i­tion.
holes3 :: Schema3 m -> [(Int, Ty­peRep)]
holes3 = fst . go 0 where
  go i (Var3 ty (Hole3 _)) = ([(i, ty)], i + 1) -- tag is ig­nored
  go i (Let3 _ b e) =
    let (bhs, i')  = go i  b
        (ehs, i'') = go i' e
    in (bhs ++ ehs, i'')
  go i (Ap3 _ f e) =
    let (fhs, i')  = go i  f
        (ehs, i'') = go i' e
    in (fhs ++ ehs, i'')
  go i _ = ([], i)

-- | Get all the named vari­ables in an ex­pres­sion.
names3 :: Exp3 m h -> [(String, Ty­peRep)]
names3 = nub . go where
  go (Var3 ty (Named3 s)) = [(s, ty)]
  go (Let3 _ b e) = go b ++ go e
  go (Ap3 _ f e) = go f ++ go e
  go _ = []

-- | Con­struct a lit­eral value.
lit3 :: String -> BDy­namic -> Exp3 m h
lit3 = Lit3

-- | Con­struct a typed hole.
hole3 :: Ty­peRep -> Schema3 m
hole3 ty = Var3 ty (Hole3 ())

-- | Per­form a func­tion ap­plic­a­tion, if type-­cor­rect.
ap3 :: Exp3 m h -> Exp3 m h -> Maybe (Exp3 m h)
ap3 f e = (\ty -> Ap3 ty f e) <$> typeOf3 f `fun­Res­ultTy` typeOf3 e

-- | Give names to holes, if type-­cor­rect.
name3 :: [(Int, String)] -> Schema3 m -> Maybe (Schema3 m)
name3 is e0 = (\(e,_,_) -> e) <$> go [] 0 e0 where
  go env i n@(Var3 ty (Named3 s)) = case lookup s env of
    Just sty
      | ty == sty -> Just (n, env, i)
      | oth­er­wise -> Nothing
    Nothing -> Just (n, env, i)
  go env i (Var3 ty (Hole3 h)) = case lookup i is of
    Just s -> case lookup s env of
      Just sty
        | ty == sty -> Just (Var3 ty (Named3 s), env, i + 1)
        | oth­er­wise -> Nothing
      Nothing -> Just (Var3 ty (Named3 s), (s,ty):env, i + 1)
    Nothing -> Just (Var3 ty (Hole3 h), env, i + 1)
  go env i (Bind3 ty b e) = do -- a new case for Bind3, the same as the case for Let3
    (b', env',  i')  <- go env  i  b
    (e', env'', i'') <- go env' i' e
    Just (Bind3 ty b' e', env'', i'')
  go env i (Let3 ty b e) = do
    (b', env',  i')  <- go env  i  b
    (e', env'', i'') <- go env' i' e
    Just (Let3 ty b' e', env'', i'')
  go env i (Ap3 ty f e) = do
    (f', env',  i')  <- go env  i  f
    (e', env'', i'') <- go env' i' e
    Just (Ap3 ty f' e', env'', i'')
  go env i e = Just (e, env, i)

-- | From a schema that may have holes, gen­erate a list of terms with named vari­ables
-- sub­sti­tuted in­stead.
terms3 :: (Ty­peRep -> Char) -> Schema3 m -> [Term3 m]
terms3 nf = map­Maybe toTerm3 . sortOn (Down . length . names3) . go where
  go e0 = case hs e0 of
    [] -> [e0]
    (chosen:_) -> con­catMap go
      [ e | ps <- par­ti­tions chosen
          , let (((_,tyc):_):_) = ps
          , let vname i = if i == 0 then [nf tyc] else nf tyc : show i
          , let naming = concat $ zip­With (\i vs -> [(v, vname i) | (v,_) <- vs]) [0..] ps
          , e <- may­beToList (name3 naming e0)
      ]

  -- holes grouped by type
  hs = groupBy ((==) `on` snd) . sortOn snd . holes3

  -- all par­ti­tions of a list
  par­ti­tions (x:xs) =
    [[x]:p | p <- par­ti­tions xs] ++
    [(x:ys):yss | (ys:yss) <- par­ti­tions xs]
  par­ti­tions [] = [[]]

Aside: Lim­ited Poly­morphism

The rep­res­ent­a­tion so far is good, and lets us ex­press everything we want, but it’s still not very friendly to use in one common case: poly­morphic mon­adic func­tions.

There are many mon­adic op­er­a­tions of the type Monad m => m a -> m (): the ac­tual type of the first ar­gu­ment is ig­nored. At the mo­ment, dealing with such terms re­quires either spe­cial­ising that a to each con­crete type used, or using some­thing like void and spe­cial­ising that.

Im­ple­menting full-blown Haskell poly­morphism would be a pain, but this is a small and ir­rit­ating enough case that it’s worth dealing with.

Presenting (trum­pets please), the “ignore” type:

-- | A spe­cial type for en­abling basic poly­morph­ism.
--
-- A func­tion para­meter of type @m Ig­nore@ uni­fies with values of any type @m a@, where @fmap
-- (const Ig­nore)@ is ap­plied to the para­meter auto­mat­ic­ally. This avoids the need to clutter
-- ex­pres­sions with calls to 'void', or some other such func­tion.
data Ig­nore = Ig­nore de­riving (Bounded, Enum, Eq, Ord, Read, Show)

Ig­nore is going to give us our lim­ited poly­morph­ism, by chan­ging the typing rules for ap3 and eval­u­ation rules for Ap3 slightly.

Ap­plic­a­tion: func­tion ap­plic­a­tion is as nor­mal, with the ex­cep­tion that if the formal para­meter has type m Ig­nore and the ac­tual para­meter has type m a, for any a, then the ap­plic­a­tion also suc­ceeds:

-- | Per­form a func­tion ap­plic­a­tion, if type-­cor­rect.
--
-- There is a spe­cial case, see the com­ment of the 'Ignore' type.
ap3ig :: forall m h. (Ap­plic­ative m, Type­able m) => Exp3 m h -> Exp3 m h -> Maybe (Exp3 m h)
ap3ig f e = case (splitTy­ConApp (typeOf3 f), splitTy­ConApp (typeOf3 e)) of
    ((_, [fargTy,fresTy]), (etyCon, et­yArgs))
      -- check if the formal para­meter is of type @m Ig­nore@ and the ac­tual para­meter is of type @m a@
      | fargTy == ig­noreTy && etyCon == mtyCon && not (null et­yArgs) && mt­yArgs == init et­yArgs -> Just (Ap3 fresTy f e)
      -- oth­er­wise try normal func­tion ap­plic­a­tion
      | oth­er­wise -> (\ty -> Ap3 ty f e) <$> typeOf3 f `fun­Res­ultTy` typeOf3 e
    _ -> Nothing
  where
    ig­noreTy = typeOf (pure Ig­nore :: m Ig­nore)
    (mtyCon, mt­yArgs) = splitTy­ConApp (ty­peRep (Proxy :: Proxy m))

Eval­u­ation: eval­u­ation of ap­plic­a­tions has an ana­logous case. When ap­plying a func­tion, the type of the formal para­metr is checked and, if it’s m Ig­nore, the ar­gu­ment gets fmap (const Ig­nore) ap­plied:

-- | Eval­uate a term
eval3ig :: forall m. (Monad m, Type­able m) => [(String, BDy­namic)] -> Term3 m -> Maybe BDy­namic
eval3ig globals e0
    | all check (names3 e0) = Just (go [] e0)
    | oth­er­wise = Nothing
  where
    go locals (Bind3 ty b e) = case (un­wrap­Functor :: BDy­namic -> Maybe (m BDy­namic)) (go locals b) of
      Just mdyn -> un­safe­Wrap­Functor ty $ mdyn >>= \dyn -> case un­wrap­Functor (go (dyn:locals) e) of
        Just dyn -> dyn
        Nothing -> error "type error I can't deal with here!"
      Nothing -> error "type error I can't deal with here!"
    go locals (Let3 _ b e) = go (go locals b : locals) e
    go locals v@(Var3 _ _) = case env locals v of
      Just dyn -> dyn
      Nothing -> error "en­vir­on­ment error I can't deal with here!"
    go locals (Ap3 _ f e) =
      let f' = go locals f
          e' = go locals e
      in case f' `bdyn­Apply` (if hasIgnoreArg f' then ig­nore e' else e') of
        Just dyn -> dyn
        Nothing -> error "type error I can't deal with here!"
    go _ (Lit3 _ dyn) = dyn

    env locals (Var3 _ (Bound3 n))
      | length locals > n = Just (locals !! n)
      | oth­er­wise = Nothing
    env _ (Var3 ty (Named3 s)) = case lookup s globals of
      Just dyn | bdyn­Ty­peRep dyn == ty -> Just dyn
      _ -> Nothing
    env _ (Var3 _ (Hole3 v)) = ab­surd v

    hasIgnoreArg fdyn =
      let (_, [fargTy,_]) = splitTy­ConApp (bdyn­Ty­peRep fdyn)
      in fargTy == ig­noreTy

    ig­nore dyn = case (un­wrap­Functor :: BDy­namic -> Maybe (m BDy­namic)) dyn of
      Just ma -> un­safeToB­Dy­namic ig­noreTy (const Ig­nore <$> ma)
      Nothing -> error "non-­mon­adic value I can't deal with here!" -- this is un­reach­able

    ig­noreTy = typeOf (pure Ig­nore :: m Ig­nore)

    check (s, ty) = case lookup s globals of
      Just dyn -> bdyn­Ty­peRep dyn == ty
      Nothing  -> False

The final piece of the puzzle is this:

-- | Con­vert an ar­bit­rary value into a dy­namic value, given its type.
--
-- This is un­safe be­cause if the type is in­cor­rect and the value is later used as that type, good
-- luck.
un­safeToB­Dy­namic :: Ty­peRep -> a -> BDy­namic
un­safeToB­Dy­namic ty = BDy­namic ty . un­sa­fe­Co­erce

And a demo:

λ> r <- newIORef (5::Int)
λ> let double = lit3 $ toB­Dy­namic ((\x -> x >> x >> pure ()) :: IO Ig­nore -> IO ()) :: Exp3 IO h
λ> let ad­dOne = lit3 $ toB­Dy­namic (modi­fyIORef r (+1)) :: Exp3 IO h
λ> let ad­dTwo = fromJust $ double `ap3ig` ad­dOne
λ> let eval = fromJust $ (fromBDy­namic :: BDy­namic -> Maybe (IO ())) =<< eval3ig [] =<< toTerm3 ad­dTwo
λ> eval
λ> readIORef r
7
λ> eval
λ> readIORef r
9