用於廣義多參數函數提升的類型技巧

我想將Haskell函數提升爲更高階的lambda微積分編碼。這幾乎是從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

我可以嵌入任意哈斯克爾類型分爲使用embLam，但我不能使用(^)申請即可。此外，解除職能將表現得很懶惰。相反，我必須通過應用程序解除它們的應用程序。

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的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中表達嗎？

來源

2013-11-21 J. Abrahamson

我不知道答案，但下一個鏈接可能會有幫助：http://hackage.haskell.org/package/layers-0.1/docs/Documentation-Layers-Overview.html – wit

您可能想看看在無tagless-final樣式中的 Ordinary and one-pass CPS transformation。訣竅是在對象語言中概括箭頭類型。我們經常在對象語言中使用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

現在我們有足夠的自由來解釋Arr，具體取決於特定的repr。被引用的文章將Arr解釋爲CPS實例。我們可以達到同樣的效果 - 爲對象語言重新定義箭頭的含義 - 不需要引入Arr類型（帶有注入問題），也不需要ES語義。上面的鏈接，對普通和單通CPS轉換，使用標準語義和重新解釋函數類型構造函數的含義來顯示新代碼。不再有任何注入問題。

來源

2013-11-23 04:28:37 Oleg

我昨晚看了這個並發現它是非常豐富的，但我需要弄清楚如何最好地通過類型家庭非注入性工作。我認爲我通常對期望太大，Haskell箭頭會持續在對象語言表示中。感謝您的迴應！ –

用於廣義多參數函數提升的類型技巧

回答

相關問題