索引單子的重新綁定符號

我正在關注Conor McBride的「Kleisli憤怒的財富箭頭」論文，並且我發佈了他的代碼here的實現。簡要地說，他定義了以下類型和類：索引單子的重新綁定符號

type a :-> b = forall i . a i -> b i 

class IFunctor f where imap :: (a :-> b) -> (f a :-> f b) 

class (IFunctor m) => IMonad m where 
    skip :: a :-> m a 
    bind :: (a :-> m b) -> (m a :-> m b) 

data (a := i) j where 
    V :: a -> (a := i) i

然後他定義了兩種類型結合的，其中後者的使用(:=)限制初始索引：

-- Conor McBride's "demonic bind" 
(?>=) :: (IMonad m) => m a i -> (a :-> m b) -> m b i 
(?>=) = flip bind 

-- Conor McBride's "angelic bind" 
(>>=) :: (IMonad m) => m (a := j) i -> (a -> m b j) -> m b i 
m >>= f = bind (\(V a) -> f a) m

後者綁定工作完全正常重新編號do表示法使用帶有RebindableSyntax擴展名的索引單子，使用return和fail的以下相應定義：

return :: (IMonad m) => a -> m (a := i) i 
return = skip . V 

fail :: String -> m a i 
fail = error

...但問題是，我不能得到前綁定（即(?>=)）工作。我試着而不是定義(>>=)和return是：

(>>=) :: (IMonad m) => m a i -> (a :-> m b) -> m b i 
(>>=) = (?>=) 

return :: (IMonad m) => a :-> m a 
return = skip

然後創建保證居住在特定的索引數據類型：

data Unit a where 
    Unit :: Unit()

但是當我嘗試使用新的定義重新綁定do符號(>>=)和return，它不起作用，如以下示例所示：

-- Without do notation 
test1 = skip Unit >>= \Unit -> skip Unit 

-- With do notation 
test2 = do 
    Unit <- skip Unit 
    skip Unit

test1型檢查，但test2沒有，這是奇怪的，因爲我覺得所有的RebindableSyntax所做的就是讓do符號desugar test2到test1，所以如果test1類型的檢查，那麼爲什麼不test2？我得到的錯誤是：當我使用顯式forall語法而不是:->型運營商的

Couldn't match expected type `t0 -> t1' 
      with actual type `a0 :-> m0 b0' 
Expected type: m0 a0 i0 -> (t0 -> t1) -> m Unit() 
    Actual type: m0 a0 i0 -> (a0 :-> m0 b0) -> m0 b0 i0 
In a stmt of a 'do' block: Unit <- skip Unit 
In the expression: 
    do { Unit <- skip Unit; 
     skip Unit }

錯誤甚至仍然存在。

現在我知道使用「惡魔綁定」還有一個問題，那就是你無法定義(>>)，但我仍然想看看我能走多遠。任何人都可以解釋爲什麼我不能讓GHC去解除「惡魔般的束縛」，即使它通常會進行類型檢查？

來源

2012-06-14 Gabriel Gonzalez

因爲這出現在一個[較新的重複問題]（http://stackoverflow.com/questions/33488322/ranknpolymorphism-and-kleisli-arrows-of-outrageous-fortune），我會指出，現在的GHC （目前爲7.10.2）幾乎完全支持'ImpredicativeTypes'，所以現在比這個代碼的'do'符號要多得多。 –

IIUC，GHC desarer實際運行後 typechecker（source）。這就解釋了爲什麼你觀察到的情況在理論上是可能的。 typechecker可能有一些特殊的鍵入規則，並且這些規則可能與typechecker在解碼代碼時所做的不一致。

當然，期望它們是一致的是合理的，所以我建議提交GHC錯誤。

來源

2012-06-16 00:19:30

感謝您的鏈接。我會檢查這一點。如果他們同意這是類型錯誤的原因，我會接受你的答案。 –

我也很想知道發生了什麼事。我面臨同樣的問題，但不那麼激動。我預計惡魔般的多態性是出乎意料的：它讓很多人感到驚訝。 – pigworker

索引單子的重新綁定符號

回答

相關問題