Polymorphism in Guest Languages

[kztk-m]

In most situations, I believe that the host (Haskell) level polymorphism suffices. However, when a guest language comes with the ability of function definitions, the lack of guest's level polymorphism becomes an issue.

Consider the following let_.

let_ :: e a -> (e a -> e b) -> e b 

This let_ cannot be used to bind a polymorphism variable for the following reasons.

• forall a. e (f a) is different from e (forall a. f a).
• Haskell disallows types like e (forall a. f a).
• The underlying theory, Atkey's unembedding, focuses on simply-typed languages (in my understanding).

I don't think that we can be happy if we have explicit manipulation of guest-level type variables from a DSL design perspective. Rather, what we want to do is to treat Haskell-level polymorphic DSL function

forall a b. e (a -> b) 

well in the framework.

Workaround on Syntax Definitions

We first focus on the two issues. Since we are not allowed to represent e (forall a. f a), we have to introduce a form of type that represents e (F a). Here, since a of e a belongs to a certain kind K rather than Type, the following limitations in Haskell are crucial.

• We can define a type synonym type F a = a ~> a but it cannot be partially applied in Haskell.
• Type declarations by data/newtype can only be used to define a type; newtype F a = MkF (a ~> a) is rejected unless a ~> a lives in Type.

A workaround is to use defunctionalization.

newtype TypeFun k = Fun Type 
data T = O | T ~> T | Forall (TypeFun k) 

-- open type family, as it is hard to limit the form of `F` of `forall a. F a` 
type family App (sym :: TypeFun k) (a :: k) :: k

class L e where 
  -- ... lam, app, let_, ...
  gen  :: (forall a. Proxy a -> e (App f a)) -> e (Forall f)
  -- Here, Proxy a is to address the issue that `a` is not determined by `App f a`
  inst :: e (Forall f) -> Proxy a -> e (App f a)

idL :: L e => e (a ~> a)
idL = lam id 

data IdType 
type instance App (Fun IdType) a = a ~> a 

ididL :: L e => e (a ~> a) 
ididL = let_ (gen idL) $ \h -> app (inst h Proxy) (inst h Proxy)

The corresponding de Bruijn term can be given as:

data Ast env a where 
  -- ...
  Gen :: (forall a. Proxy a -> Ast env (App f a)) -> Ast env (Forall f) 
  Inst :: Ast env (Forall f) -> Proxy a -> Ast env (App f a) 

Issues

Currently, the framework does not provide a function to lift Gen, while its lifting can be achieved by directly using EnvI.

gen e = EnvI $ \tenv -> Gen (\p -> runEnvI (e p) tenv)

I believe that this has no issue: for an AST node having infinitely many children would not affect the bijective correspondence.

Another issue is it is rather tedious to prepare types, especially for types where more than one type variable is universally quantified, like forall a b. e (a ~> b ~> a).