广义多参数函数提升的类型类技巧

Question

我想在高阶lambda演算编码中提升一个Haskell函数。这几乎是一字不差地取自奥列格的类型化无标记最终编码。

class Lam r where
  emb :: a -> r a
  (^) :: r (r a -> r a) -> (r a -> r a)
  lam :: (r a -> r a) -> r (r a -> r a)

instance Lam Identity where
  emb   = Identity
  f ^ x = f >>= ($ x)
  lam f = return (f . return =<<) -- call-by-value

 eval = runIdentity

我可以使用emb将任意的Haskell类型嵌入到Lam中，但不能使用(^)作为应用程序。此外，取消的函数将表现为惰性。相反，我必须逐个提升它们的应用程序。

emb1 :: ( Applicative r, Lam r ) 
     => (a -> b) -> r (r a -> r b)
emb1 f = lam $ \ra -> f <$> ra

emb2 :: ( Applicative r, Lam r ) 
     => (a -> b -> c) -> r (r a -> r (r b -> r c))
emb2 f = lam $ \ra -> lam $ \rb -> f <$> ra <*> rb

emb3 :: ( Applicative r, Lam r ) 
     => (a -> b -> c -> d) 
     -> r (r a -> r (r b -> r (r c -> r d)))
emb3 f = lam $ \ra -> lam $ \rb -> lam $ \rc -> f <$> ra <*> rb <*> rc

>>> eval $ emb2 (+) ^ emb 1 ^ emb 2
3

不过，这是一个很大的样板。我想创建一个通用的提升函数，它适用于任何any函数。我觉得可以使用类似于Printf的PrintfType或fixed-vector的Cont类型，我可以使用类型函数来指定我想要的类型

type family   Low    h      o
type instance Low    ()     o =   o
type instance Low    (a, h) o =   a ->    Low    h o

type family   Lift r h      o
type instance Lift r ()     o =   o
type instance Lift r (a, h) o = r a -> r (Lift r h o)

class Emb r h o where
  embed :: Low h o -> r (Lift r h o)

instance ( Lam r ) => Emb r () o where
  embed = emb

instance ( Lam r, Applicative r, Emb r h o ) => Emb r (a, h) o where
  embed = ?

但是我被这种方法卡住了，通常是因为注入性问题。我能够使用newtype包装器和作用域类型变量的真正可怕的组合来解决注入性问题，但它从未进行过实际的类型检查。

这可以用Haskell来表达吗？

Answer 1

您可能希望以无标记的最终样式查看Ordinary and one-pass CPS transformation。诀窍是在对象语言中泛化Arrow类型。我们经常在(要嵌入的)对象语言中为函数类型使用Haskell的类型构造函数->，这一事实是巧合和方便的。通常，对象函数不会简单地映射到Haskell函数。参考文章中的代码包含ESymantics

-- How to interpret arrows and other types
type family Arr (repr :: * -> *) (a :: *) (b :: *) :: *

class ESymantics repr where
    int :: Int  -> repr Int
    add :: repr Int  -> repr Int -> repr Int

    lam :: (repr a -> repr b) -> repr (Arr repr a b)
    app :: repr (Arr repr a b) -> repr a -> repr b

现在，我们有足够的自由来根据特定的repr来解释Arr。参考文章解释了CPS实例的Arr。

Arr编辑：事实证明，我们可以达到同样的效果--重新定义对象语言的箭头含义--而无需引入类型(及其注入性问题)，也无需ESemantics。上面的链接指向普通CPS转换和一遍CPS转换，显示了新代码，使用了标准语义并重新解释了函数类型构造函数的含义。不再有任何内射性问题。