一般化されたマルチパラメータ関数のリフティングのための型抜きのトリック

Question

高次ラムダ計算のエンコーディングでHaskell関数を持ち上げたい。これはOlegのTyped Tagless Finalのエンコーディングとほぼ同じです。

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を使用してLamに、任意のHaskellの種類を埋め込むことができますが、私は、アプリケーションのための(^)を使用することはできません。さらに、持ち上げられた関数は遅延して動作します。代わりに、私はそれらをアプリケーションごとに持ち上げなければなりません。

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 

これは多くの定型文です。私は任意のアリティ機能のために働く一般的な持ち上げ機能を作りたいと思います。 PrintfのPrintfTypeやfixed-vectorののようなものを使用することが可能なような気がします。私は型の関数

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 = ? 

を使用したいが、私は非常に通常伴う単射の問題のために、このメソッドを介して動けなくなるかを指定することができます。私は新タイプのラッパーとスコープ付きの型変数の本当にぞっとした組み合わせで注入性を解決することができましたが、実際にはチェックされません。

これは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を解釈します。

編集：では結局のところ、我々は同じ効果を達成することができます - オブジェクト言語のための矢印の意味を再定義 - （その単射の問題で）とESemanticsずに編曲タイプを導入することなく。上のリンクは、標準的なセマンティクスを使用して、関数型コンストラクタの意味を再解釈する新しいコードを示しています。もはや注入性の問題はありません。