高次ラムダ計算のエンコーディングで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で表現できますか?
私は答えは分かりませんが、次のリンクが参考になります:http://hackage.haskell.org/package/layers-0.1/docs/Documentation-Layers-Overview.html – wit