RankNpolymorphism和kleisli的離譜財富箭頭

我不明白爲什麼demonbind1的定義會產生一些編譯器錯誤。它看起來像一個愚蠢的翻轉，但不知何故..RankNpolymorphism和kleisli的離譜財富箭頭

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE RankNTypes, ScopedTypeVariables, TypeOperators, TypeFamilies,ImpredicativeTypes #-} 

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) 


-- Conor McBride's "demonic bind" 
(?>=) :: forall m a b i. (IFunctor m, IMonad m) => m a i -> (a :-> m b) -> m b i 
(?>=) = 
    let 
    -- OK 
    demonbind0 = flip (bind :: forall i. (forall j. a j -> m b j) -> m a i -> m b i) 
    -- KO - see error below 
    demonbind1 = flip bind :: forall i. m a i -> (forall j. a j -> m b j) -> m b i 

    -- So i have to write this 
    demonbind2 :: forall i. (m a i -> (a :-> m b) -> m b i) 
    demonbind2 mai ti = (bind ti) mai 
    in demonbind2

的錯誤是

Couldn't match type ‘a j0 -> m b j0’ … 
       with ‘forall i2. a i2 -> m b i2’ 
    Expected type: (a j0 -> m b j0) -> m a i1 -> m b i1 
     Actual type: a :-> m b -> m a i1 -> m b i1 
In the first argument of ‘flip’, namely ‘bind’ 
    In the expression: 
     flip bind :: forall i. m a i -> (forall j. a j -> m b j) -> m b i

來源

2015-11-02 nicolas

其重複，對不起。 – nicolas

實際上，它不*相當*重複。在原來的問題中，唯一不起作用的是「做」符號。但是現在，GHC的'ImpredicativeTypes'擴展幾乎完全不起作用，所以*代碼中的所有內容都會中斷。即使使用你的'demonbind2'定義，我認爲你會很難使用*'（？> =）'。 –

是真的，不是真的重複。我將繼續進行手動擴展。這實際上是一個小傷害。現在令人討厭的是，你會希望*這樣簡單的操作即可開箱即用。 – nicolas

出人意料的是，ImpredicativeTypes似乎比平常的GHC 8.0的開發快照破碎少！這彙編沒有錯誤：

(?>=) :: (IFunctor m, IMonad m) => m a i -> (a :-> m b) -> m b i 
(?>=) = flip bind

我想知道什麼樣的改變解決了這個問題。

來源

2016-03-23 01:18:22

這是令人驚訝的，而且我認爲，大多數情況並非如此。我記得有人提到一些新的「ImpredicativeTypes」破碎。最近對類型系統進行了重大改變的理查德·艾森伯格迴應說，他沒有做任何努力來避免進一步破壞已經被打破的擴展。 – dfeuer

@dfeuer我沒有說'ImpredicativeTypes'現在工作。我只是說他們*看起來*少了*，這是完全不同的說法。他們肯定不應該使用，直到他們得到適當的修復。 –

從積極的方面來看，似乎正在開展一些工作：https：//ghc.haskell.org/trac/ghc/raw-attachment/wiki/ImpredicativePolymorphism/Impredicative-2015/impredicativity.pdf –

RankNpolymorphism和kleisli的離譜財富箭頭

回答

相關問題