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

This is a simplified version of a problem I’ve been having in CoCo. The current handling of variables in CoCo is very poor, the programmer has to specify exactly which variables may be introduced, binds and lets cause shadowing, and no care is taken to avoid generating alpha equivalent terms.

Here are two representative problems:

If you have the variable

`x`

, and no others, a term like this will not be generated:`f >>= \x1 -> g x1 x`

If you have the variables

`x`

and`y`

of the same type, these equivalent terms will be generated:`f x`

and`f y`

Let’s get started…

{-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} import Data.Dynamic (Dynamic, dynApply, dynTypeRep) import Data.Function (on) import Data.List (groupBy, nub, sortOn) import Data.Maybe (mapMaybe, maybeToList) import Data.Ord (Down(..)) import Data.Proxy (Proxy(..)) import Data.Typeable (Typeable, TypeRep, funResultTy, splitTyConApp, typeOf, typeRep) import Data.Void (Void, absurd) import GHC.Exts (Any) import Unsafe.Coerce (unsafeCoerce)

## Mark 1: A Simple Typed Expression Type

Our expressions are representations of Haskell code, which makes this a bit unlike most toy expression evaluators you see in tutorials. We want everything to be very typed, and not expose the constructors of the expression data type, using smart constructors to ensure that only well-typed expressions can be created.

It’s this typing that makes it really difficult to use the bound library here, as bound doesn’t play so nicely with typed variables. You can infer types for variables later, but I don’t really want to implement that.

-- | A type for expressions. This would not be exported by actual library code, to prevent the user -- from mucking around with the types. data Exp1 = Lit1 String Dynamic -- ^ Literal values are just dynamically-wrapped Haskell values. | Hole1 TypeRep -- ^ "Holes" are free variables, identified by their position in the tree. | Named1 TypeRep String -- ^ Variables which are bound by a provided environment. More on this later. | Bound1 TypeRep Int -- ^ Variables which are bound by a let, with de Bruijn indices. All variables bound to the same -- let must have the correct type. | Let1 TypeRep Exp1 Exp1 -- ^ The binder is assumed to be of the correct type for all the variables bound to it. | Ap1 TypeRep Exp1 Exp1 -- ^ The parameter is assumed to be of the correct type for the function. instance 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 expression. typeOf1 :: Exp1 -> TypeRep typeOf1 (Lit1 _ dyn) = dynTypeRep 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 expression, identified by position. holes1 :: Exp1 -> [(Int, TypeRep)] 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 variables in an expression. names1 :: Exp1 -> [(String, TypeRep)] 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 constructors**: we only want to be able to produce type-correct expressions, for two reasons: the evaluator in CoCo is more complex and does a lot of unsafe coercion, and being able to just call `error`

when the types don’t work out is nicer than needing to actually handle it; and it makes it easier to generate terms programmatically, as you simply try all possibilities and keep the ones which succeed.

-- | Construct a literal value. lit1 :: String -> Dynamic -> Exp1 lit1 = Lit1 -- | Construct a typed hole. hole1 :: TypeRep -> Exp1 hole1 = Hole1 -- | Perform a function application, if type-correct. ap1 :: Exp1 -> Exp1 -> Maybe Exp1 ap1 f e = (\ty -> Ap1 ty f e) <$> typeOf1 f `funResultTy` typeOf1 e -- | Bind a collection of holes, if type-correct. -- -- The binding is applied "atomically", in that you don't need to worry about holes disappearing and -- so changing their position-indices while this operation happens; however the position of unbound -- holes may be altered in the result of this function. 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 | otherwise = 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-correct. -- -- This has the same indexing behaviour 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) | otherwise -> 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) | otherwise -> 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)

**Evaluation**: now we have everything in place to evaluate expressions with no unbound holes. Everything is type-correct-by-construction, so if there are no holes (and the global environment has everything we need) we can get out a value.

-- | Evaluate an expression if it has no holes. eval1 :: [(String, Dynamic)] -> Exp1 -> Maybe Dynamic eval1 globals = go [] where -- the local environment is a list of values, with each new scope prepending a value; this means -- that the de Bruijn indices correspond with list indices go locals (Let1 _ b e) = (\dyn -> go (dyn:locals) e) =<< go locals b go locals (Bound1 _ n) = Just (locals !! n) -- named variables come from the global environment go _ (Named1 ty s) = case lookup s globals of Just dyn | dynTypeRep dyn == ty -> Just dyn _ -> Nothing -- the other operations don't care about either environment go locals (Ap1 _ f e) = do dynf <- go locals f dyne <- go locals e dynf `dynApply` dyne go _ (Lit1 _ dyn) = Just dyn go _ (Hole1 _) = Nothing

**Removing Holes**: we still have one more problem, it would be nice for holes to be given names automatically, and not just individual holes, but groups of holes too.

For example, if we have an expression like so:

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

It would be nice to be able to generate these expressions automatically:

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 particularly nice if they were generated in a list in that order, from most free to most constrained.

-- | From an expression that may have holes, generate a list of expressions with named variables -- substituted instead, ordered from most free (one hole per variable) to most constrained (multiple -- holes per variable). -- -- This takes a function to assign a letter to each type, subsequent variables of the same type have -- digits appended. terms1 :: (TypeRep -> Char) -> Exp1 -> [Exp1] terms1 nf = sortOn (Down . length . names1) . go where go e0 = case hs e0 of [] -> [e0] (chosen:_) -> concatMap go [ e | ps <- partitions chosen , let (((_,tyc):_):_) = ps , let vname i = if i == 0 then [nf tyc] else nf tyc : show i , let naming = concat $ zipWith (\i vs -> [(v, vname i) | (v,_) <- vs]) [0..] ps , e <- maybeToList (name1 naming e0) ] -- holes grouped by type hs = groupBy ((==) `on` snd) . sortOn snd . holes1 -- all partitions of a list partitions (x:xs) = [[x]:p | p <- partitions xs] ++ [(x:ys):yss | (ys:yss) <- partitions xs] partitions [] = [[]]

Here’s an example from ghci:

λ> let intHole = hole1 $ T.typeOf (5::Int) λ> let boolHole = hole1 $ T.typeOf True λ> let ibf = lit1 "f" (D.toDyn ((\_ _ _ a -> a) :: Int -> Bool -> Bool -> Int -> Int)) λ> let ibfExp = fromJust $ do { x <- ibf `ap1` intHole; y <- x `ap1` boolHole; z <- y `ap1` boolHole; z `ap1` intHole } λ> mapM_ print $ terms1 (head.show) ibfExp ((((f) ((I :: Int))) ((B :: Bool))) ((B1 :: Bool))) ((I1 :: Int)) ((((f) ((I :: Int))) ((B :: Bool))) ((B1 :: Bool))) ((I :: Int)) ((((f) ((I :: Int))) ((B :: Bool))) ((B :: Bool))) ((I1 :: Int)) ((((f) ((I :: Int))) ((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 desired: it would be nice to be able to statically forbid passing expressions with holes to `eval`

. As always in Haskell, the solution is to add another type parameter.

data Exp2 h = Lit2 String Dynamic | Var2 TypeRep (Var2 h) -- ^ One constructor for holes, named, and bound variables. | Let2 TypeRep (Exp2 h) (Exp2 h) | Ap2 TypeRep (Exp2 h) (Exp2 h) instance 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 -- ^ Environment variables. | Bound2 Int -- ^ Let-bound variables. instance 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, actually, it lets us very simply forbid the presence of holes! Constructing an `h`

value is required to construct a hole, so if we set it to `Void`

, then no holes can be made at all! If the tag is some inhabited type, then an expression may contain holes (but may not).

Let’s introduce two type synonyms to talk about these:

-- | A schema is an expression which may contain holes. A single schema may correspond to many -- terms. type Schema2 = Exp2 () -- | A term is an expression with no holes. Many terms may correspond to a single schema. type Term2 = Exp2 Void -- | Convert 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

**Evaluation & Hole Removal**: now we can evaluate *terms* after removing holes from *schemas*. Statically-checked guarantees that we’re dealing with all of our holes properly, nice!

-- | Evaluate a term eval2 :: [(String, Dynamic)] -> Term2 -> Maybe Dynamic 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 `dynApply` dyne go _ (Lit2 _ dyn) = Just dyn env locals (Var2 _ (Bound2 n)) | length locals > n = Just (locals !! n) | otherwise = Nothing env _ (Var2 ty (Named2 s)) = case lookup s globals of Just dyn | dynTypeRep dyn == ty -> Just dyn _ -> Nothing env _ (Var2 _ (Hole2 v)) = absurd v -- this is actually unreachable now -- | From a schema that may have holes, generate a list of terms with named variables -- substituted instead. terms2 :: (TypeRep -> Char) -> Schema2 -> [Term2] terms2 nf = mapMaybe toTerm2 . sortOn (Down . length . names2) . go where go e0 = case hs e0 of [] -> [e0] (chosen:_) -> concatMap go [ e | ps <- partitions chosen , let (((_,tyc):_):_) = ps , let vname i = if i == 0 then [nf tyc] else nf tyc : show i , let naming = concat $ zipWith (\i vs -> [(v, vname i) | (v,_) <- vs]) [0..] ps , e <- maybeToList (name2 naming e0) ] -- holes grouped by type hs = groupBy ((==) `on` snd) . sortOn snd . holes2 -- all partitions of a list partitions (x:xs) = [[x]:p | p <- partitions xs] ++ [(x:ys):yss | (ys:yss) <- partitions xs] partitions [] = [[]]

The rest of the code hasn’t changed much, but is included for completeness:

-- | Get the type of an expression. typeOf2 :: Exp2 h -> TypeRep typeOf2 (Lit2 _ dyn) = dynTypeRep dyn typeOf2 (Var2 ty _) = ty typeOf2 (Let2 ty _ _) = ty typeOf2 (Ap2 ty _ _) = ty -- | Get all the holes in an expression, identified by position. holes2 :: Schema2 -> [(Int, TypeRep)] holes2 = fst . go 0 where go i (Var2 ty (Hole2 _)) = ([(i, ty)], i + 1) -- tag is ignored 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 variables in an expression. names2 :: Exp2 h -> [(String, TypeRep)] 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 _ = [] -- | Construct a literal value. lit2 :: String -> Dynamic -> Exp2 h lit2 = Lit2 -- | Construct a typed hole. hole2 :: TypeRep -> Schema2 hole2 ty = Var2 ty (Hole2 ()) -- holes get tagged with unit -- | Perform a function application, if type-correct. ap2 :: Exp2 h -> Exp2 h -> Maybe (Exp2 h) ap2 f e = (\ty -> Ap2 ty f e) <$> typeOf2 f `funResultTy` typeOf2 e -- | Bind a collection of holes, if type-correct. 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 ignored | otherwise = Just (Var2 ty (Hole2 h), i + 1) -- tag is preserved 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-correct. 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) | otherwise -> 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 ignored | otherwise -> Nothing Nothing -> Just (Var2 ty (Named2 s), (s,ty):env, i + 1) -- tag is ignored Nothing -> Just (Var2 ty (Hole2 h), env, i + 1) -- tag is preserved 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 Implementation of Data.Dynamic

In the Mark 3 evaluator, we’re going to need a function of type `Monad m => m Dynamic -> Dynamic`

, which “pushes” the `m`

inside the `Dynamic`

, and of type `Monad m => Dynamic -> Maybe (m Dynamic)`

. Unfortunately, Data.Dynamic doesn’t provide a way to do this, for good reason: it’s impossible in general! There’s no way to know what the type of the dynamic value inside the monad is, so there’s no way to do this safely.

Fortunately, implementing a Data.Dynamic-lite is pretty simple.

-- | A dynamic value is a pair of its type and 'Any'. Any is a magical type which is guaranteed to -- | work with 'unsafeCoerce'. data BDynamic = BDynamic { bdynTypeRep :: TypeRep, bdynAny :: Any } instance Show BDynamic where show = show . bdynTypeRep

(`BDynamic`

for “barrucadu’s dynamic”)

We need to be able to construct and deconstruct dynamic values, these operations do use `unsafeCoerce`

, but are safe:

-- | Convert an arbitrary value into a dynamic one. toBDynamic :: Typeable a => a -> BDynamic toBDynamic a = BDynamic (typeOf a) (unsafeCoerce a) -- | Convert a dynamic value into an ordinary value, if the types match. fromBDynamic :: Typeable a => BDynamic -> Maybe a fromBDynamic (BDynamic ty v) = case unsafeCoerce v of -- this is a bit mind-bending, but the 'typeOf r' here is the type of the 'a', as 'unsafeCoerce -- v :: a' (regardless of whether it actually is an 'a' value or not). The same result could be -- achieved using ScopedTypeVariables and 'typeRep'. r | ty == typeOf r -> Just r | otherwise -> Nothing

The final operation needed for the Marks 1 and 2 implementation is function application:

-- | Dynamically-typed function application. bdynApply :: BDynamic -> BDynamic -> Maybe BDynamic bdynApply (BDynamic ty1 f) (BDynamic ty2 x) = case funResultTy ty1 ty2 of Just ty3 -> Just (BDynamic ty3 ((unsafeCoerce f) x)) Nothing -> Nothing

Now we can construct our strange monad-shuffling operations:

-- | "Push" a functor inside a dynamic value, given the type of the resultant value. -- -- This is unsafe because if the type is incorrect and the value is later used as that type, good -- luck. unsafeWrapFunctor :: Functor f => TypeRep -> f BDynamic -> BDynamic unsafeWrapFunctor ty fdyn = BDynamic ty (unsafeCoerce $ fmap bdynAny fdyn) -- | "Extract" a functor from a dynamic value. unwrapFunctor :: forall f. (Functor f, Typeable f) => BDynamic -> Maybe (f BDynamic) unwrapFunctor (BDynamic ty v) = case splitTyConApp ty of (tyCon, tyArgs) | tyCon == ftyCon && not (null tyArgs) && init tyArgs == ftyArgs -> Just $ BDynamic (last tyArgs) <$> unsafeCoerce v _ -> Nothing where (ftyCon, ftyArgs) = splitTyConApp (typeRep (Proxy :: Proxy f))

It’s almost a shame that Data.Dynamic doesn’t expose enough to implement this. It has gone for a safe but limited API. A common Haskell “design” pattern is to have safe public APIs and unsafe but publically-exposed “internal” APIs, but base doesn’t seem to follow that.

## Mark 3: Monadic Expressions

This expression representation is pretty nice, but it’s rather cumbersome to express monadic operations for a couple of reasons:

Everything is monomorphic, so there would need to be a separate

`lit`

for`>>=`

at every desired type.Due to function application having a

`Maybe`

result, even at a single type writing`ap2 (lit2 ((>>=) :: Type)) e1 >>= \f -> ap2 f e2`

is not nice.The original need for this expression representation was for generating Haskell terms, and generating lambda terms is tricky; it would be nice to be able to bind holes directly.

This calls for a third representation of expressions. For reasons that will become apparent when looking at the evaluator, we’ll specalise this to only working in one monad, and track the monad type as another parameter of `Exp`

:

data Exp3 (m :: * -> *) (h :: *) = Lit3 String BDynamic | Var3 TypeRep (Var3 h) | Bind3 TypeRep (Exp3 m h) (Exp3 m h) | Let3 TypeRep (Exp3 m h) (Exp3 m h) | Ap3 TypeRep (Exp3 m h) (Exp3 m h) instance 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 ++ ")"

**Construction**: bind is going to be treated just as a let with special evaluation rules. This means that de Bruijn indices will be able to refer to a bind or a let. Rather than have two separate counters for those, we’ll just put everything in the same namespace (index-space?).

-- | Bind a collection of holes, if type-correct. let3 :: [Int] -> Schema3 m -> Schema3 m -> Maybe (Schema3 m) let3 is b e0 = Let3 (typeOf3 e0) b <$> letOrBind3 is (typeOf3 b) e0 -- | Monadically bind a collection of holes, if type-correct. -- -- This has the same indexing behaviour as 'let3'. bind3 :: forall m. Typeable m => [Int] -> Schema3 m -> Schema3 m -> Maybe (Schema3 m) bind3 is b e0 = case (splitTyConApp (typeOf3 b), splitTyConApp (typeOf3 e0)) of ((btyCon, btyArgs), (etyCon, etyArgs)) | btyCon == mtyCon && btyCon == etyCon && not (null btyArgs) && not (null etyArgs) && mtyArgs == init btyArgs && init btyArgs == init etyArgs -> Bind3 (typeOf3 e0) b <$> letOrBind3 is (last btyArgs) e0 _ -> Nothing where (mtyCon, mtyArgs) = splitTyConApp (typeRep (Proxy :: Proxy m)) -- | A helper for 'bind3' and 'let3': bind holes to the top of the expression. letOrBind3 :: [Int] -> TypeRep -> Exp3 m h -> Maybe (Exp3 m h) letOrBind3 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 | otherwise = 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 `letOrBind3`

also work for `name3`

by carrying around a third state token and letting the `Var3`

case apply an arbitrary function.

**Evaluation**: the new bind case, unfortunately, complicates things somewhat here. It’s *much* more awkward to deal with errors during evaluation, but fortunately the only errors that can actually arise are unbound named variables: the smart constructors ensure expressions are well-typed and have valid de Bruijn indices. This means we can just check the named variables for validity up front and then use `error`

once we’re sure there actually are no errors.

-- | Evaluate a term eval3 :: forall m. (Monad m, Typeable m) => [(String, BDynamic)] -> Term3 m -> Maybe BDynamic eval3 globals e0 | all check (names3 e0) = Just (go [] e0) | otherwise = Nothing where go locals (Bind3 ty b e) = case (unwrapFunctor :: BDynamic -> Maybe (m BDynamic)) (go locals b) of Just mdyn -> unsafeWrapFunctor ty $ mdyn >>= \dyn -> case unwrapFunctor (go (dyn:locals) e) of Just dyn -> dyn Nothing -> error "type error I can't deal with here!" -- this is unreachable Nothing -> error "type error I can't deal with here!" -- this is unreachable 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 "environment error I can't deal with here!" -- this is unreachable go locals (Ap3 _ f e) = case go locals f `bdynApply` go locals e of Just dyn -> dyn Nothing -> error "type error I can't deal with here!" -- this is unreachable go _ (Lit3 _ dyn) = dyn env locals (Var3 _ (Bound3 n)) | length locals > n = Just (locals !! n) | otherwise = Nothing env _ (Var3 ty (Named3 s)) = case lookup s globals of Just dyn | bdynTypeRep dyn == ty -> Just dyn _ -> Nothing env _ (Var3 _ (Hole3 v)) = absurd v check (s, ty) = case lookup s globals of Just dyn -> bdynTypeRep dyn == ty Nothing -> False

Now it becomes apparent why the monad type parameter is needed in the expression type, the evaluator uses `>>=`

, and so it needs to know which monad to bind it as. An alternative would be to use a type like this, but this still restricts you to using a single monad and so doesn’t gain anything:

eval3alt :: (Monad m, Typeable m) => proxy m -> [(String, BDynamic)] -> Term3 -> Maybe BDynamic

Here’s a little example showing that side-effects do work (when I first did this, they didn’t, so it’s not quite trivial to get right):

λ> r <- newIORef (5::Int) λ> let intHole = hole3 $ T.typeOf (5::Int) λ> let plusLit = lit3 "+" . toBDynamic $ ((+) :: Int -> Int -> Int) λ> let plusTwo = fromJust $ (fromJust $ plusLit `ap3` intHole) `ap3` intHole λ> let pureInt = lit3 "pure" . toBDynamic $ (pure :: Int -> IO Int) λ> let plusTwoIO = fromJust $ pureInt `ap3` plusTwo λ> let intAndTimes = (lit3 "*2" . toBDynamic $ (modifyIORef r (*7) >> pure (7::Int))) :: Exp3 IO h λ> let eval = fromJust $ (fromBDynamic :: BDynamic -> Maybe (IO Int)) =<< eval3 [] =<< toTerm3 =<< bind3 [0,1] intAndTimes plusTwoIO λ> eval 14 λ> readIORef r 7 λ> eval 14 λ> readIORef r 49

Again, the rest of the code hasn’t changed much, but is included for completeness.

data Var3 h = Hole3 h | Named3 String | Bound3 Int instance Show (Var3 h) where show (Hole3 _) = "_" show (Named3 s) = s show (Bound3 i) = show i -- | A schema is an expression which may contain holes. type Schema3 m = Exp3 m () -- | A term is an expression with no holes. type Term3 m = Exp3 m Void -- | Convert 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 expression. typeOf3 :: Exp3 m h -> TypeRep typeOf3 (Lit3 _ dyn) = bdynTypeRep dyn typeOf3 (Var3 ty _) = ty typeOf3 (Bind3 ty _ _) = ty typeOf3 (Let3 ty _ _) = ty typeOf3 (Ap3 ty _ _) = ty -- | Get all the holes in an expression, identified by position. holes3 :: Schema3 m -> [(Int, TypeRep)] holes3 = fst . go 0 where go i (Var3 ty (Hole3 _)) = ([(i, ty)], i + 1) -- tag is ignored 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 variables in an expression. names3 :: Exp3 m h -> [(String, TypeRep)] 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 _ = [] -- | Construct a literal value. lit3 :: String -> BDynamic -> Exp3 m h lit3 = Lit3 -- | Construct a typed hole. hole3 :: TypeRep -> Schema3 m hole3 ty = Var3 ty (Hole3 ()) -- | Perform a function application, if type-correct. ap3 :: Exp3 m h -> Exp3 m h -> Maybe (Exp3 m h) ap3 f e = (\ty -> Ap3 ty f e) <$> typeOf3 f `funResultTy` typeOf3 e -- | Give names to holes, if type-correct. 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) | otherwise -> 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) | otherwise -> 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, generate a list of terms with named variables -- substituted instead. terms3 :: (TypeRep -> Char) -> Schema3 m -> [Term3 m] terms3 nf = mapMaybe toTerm3 . sortOn (Down . length . names3) . go where go e0 = case hs e0 of [] -> [e0] (chosen:_) -> concatMap go [ e | ps <- partitions chosen , let (((_,tyc):_):_) = ps , let vname i = if i == 0 then [nf tyc] else nf tyc : show i , let naming = concat $ zipWith (\i vs -> [(v, vname i) | (v,_) <- vs]) [0..] ps , e <- maybeToList (name3 naming e0) ] -- holes grouped by type hs = groupBy ((==) `on` snd) . sortOn snd . holes3 -- all partitions of a list partitions (x:xs) = [[x]:p | p <- partitions xs] ++ [(x:ys):yss | (ys:yss) <- partitions xs] partitions [] = [[]]

## Aside: Limited Polymorphism

The representation so far is good, and lets us express everything we want, but it’s still not very friendly to use in one common case: polymorphic monadic functions.

There are many monadic operations of the type `Monad m => m a -> m ()`

: the actual type of the first argument is ignored. At the moment, dealing with such terms requires either specialising that `a`

to each concrete type used, or using something like `void`

and specialising *that*.

Implementing full-blown Haskell polymorphism would be a pain, but this is a small and irritating enough case that it’s worth dealing with.

Presenting (trumpets please), the “ignore” type:

-- | A special type for enabling basic polymorphism. -- -- A function parameter of type @m Ignore@ unifies with values of any type @m a@, where @fmap -- (const Ignore)@ is applied to the parameter automatically. This avoids the need to clutter -- expressions with calls to 'void', or some other such function. data Ignore = Ignore deriving (Bounded, Enum, Eq, Ord, Read, Show)

`Ignore`

is going to give us our limited polymorphism, by changing the typing rules for `ap3`

and evaluation rules for `Ap3`

slightly.

**Application**: function application is as normal, with the exception that if the formal parameter has type `m Ignore`

and the actual parameter has type `m a`

, for any `a`

, then the application also succeeds:

-- | Perform a function application, if type-correct. -- -- There is a special case, see the comment of the 'Ignore' type. ap3ig :: forall m h. (Applicative m, Typeable m) => Exp3 m h -> Exp3 m h -> Maybe (Exp3 m h) ap3ig f e = case (splitTyConApp (typeOf3 f), splitTyConApp (typeOf3 e)) of ((_, [fargTy,fresTy]), (etyCon, etyArgs)) -- check if the formal parameter is of type @m Ignore@ and the actual parameter is of type @m a@ | fargTy == ignoreTy && etyCon == mtyCon && not (null etyArgs) && mtyArgs == init etyArgs -> Just (Ap3 fresTy f e) -- otherwise try normal function application | otherwise -> (\ty -> Ap3 ty f e) <$> typeOf3 f `funResultTy` typeOf3 e _ -> Nothing where ignoreTy = typeOf (pure Ignore :: m Ignore) (mtyCon, mtyArgs) = splitTyConApp (typeRep (Proxy :: Proxy m))

**Evaluation**: evaluation of applications has an analogous case. When applying a function, the type of the formal parametr is checked and, if it’s `m Ignore`

, the argument gets `fmap (const Ignore)`

applied:

-- | Evaluate a term eval3ig :: forall m. (Monad m, Typeable m) => [(String, BDynamic)] -> Term3 m -> Maybe BDynamic eval3ig globals e0 | all check (names3 e0) = Just (go [] e0) | otherwise = Nothing where go locals (Bind3 ty b e) = case (unwrapFunctor :: BDynamic -> Maybe (m BDynamic)) (go locals b) of Just mdyn -> unsafeWrapFunctor ty $ mdyn >>= \dyn -> case unwrapFunctor (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 "environment error I can't deal with here!" go locals (Ap3 _ f e) = let f' = go locals f e' = go locals e in case f' `bdynApply` (if hasIgnoreArg f' then ignore 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) | otherwise = Nothing env _ (Var3 ty (Named3 s)) = case lookup s globals of Just dyn | bdynTypeRep dyn == ty -> Just dyn _ -> Nothing env _ (Var3 _ (Hole3 v)) = absurd v hasIgnoreArg fdyn = let (_, [fargTy,_]) = splitTyConApp (bdynTypeRep fdyn) in fargTy == ignoreTy ignore dyn = case (unwrapFunctor :: BDynamic -> Maybe (m BDynamic)) dyn of Just ma -> unsafeToBDynamic ignoreTy (const Ignore <$> ma) Nothing -> error "non-monadic value I can't deal with here!" -- this is unreachable ignoreTy = typeOf (pure Ignore :: m Ignore) check (s, ty) = case lookup s globals of Just dyn -> bdynTypeRep dyn == ty Nothing -> False

The final piece of the puzzle is this:

-- | Convert an arbitrary value into a dynamic value, given its type. -- -- This is unsafe because if the type is incorrect and the value is later used as that type, good -- luck. unsafeToBDynamic :: TypeRep -> a -> BDynamic unsafeToBDynamic ty = BDynamic ty . unsafeCoerce

And a demo:

λ> r <- newIORef (5::Int) λ> let double = lit3 $ toBDynamic ((\x -> x >> x >> pure ()) :: IO Ignore -> IO ()) :: Exp3 IO h λ> let addOne = lit3 $ toBDynamic (modifyIORef r (+1)) :: Exp3 IO h λ> let addTwo = fromJust $ double `ap3ig` addOne λ> let eval = fromJust $ (fromBDynamic :: BDynamic -> Maybe (IO ())) =<< eval3ig [] =<< toTerm3 addTwo λ> eval λ> readIORef r 7 λ> eval λ> readIORef r 9