Neubindende Notation für indizierte Monaden

Question

Ich folgte Conor McBride's "Kleisli Pfeile des unerhörten Vermögens" Papier und ich habe meine Implementierung seines Codes here veröffentlicht. Kurz gesagt, definiert er die folgenden Typen und Klassen:

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 

Dann legt er zwei Arten von Bindungen, von denen die letztere (:=) den Anfangsindex zu beschränken verwendet:

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

Letztere binden funktioniert völlig in Ordnung für rebinding do Notation indexieren Monaden mit der RebindableSyntax Erweiterung zu verwenden, mit den folgenden entsprechenden Definitionen für return und fail:

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

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

... aber das Problem ist, dass ich die frühere Bindung nicht bekommen kann (d. H. (?>=)) zu arbeiten. Ich habe versucht zu definieren, anstatt (>>=) und return zu sein:

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

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

Dann habe ich einen Datentyp erstellt garantiert einen bestimmten Index bewohnen:

data Unit a where 
    Unit :: Unit() 

Aber wenn ich versuche do Notation mit den neuen Definitionen erneut zu binden für (>>=) und return, funktioniert es nicht, wie im folgenden Beispiel gezeigt:

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

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

test1 Typ-Kontrollen, aber test2 nicht, was seltsam ist, da ich die RebindableSyntax alles gedacht wurde, do Notation desugar ließ test2-test1, also wenn test1 Typ-Kontrollen, warum dann nicht test2 tut? Der Fehler, den ich bekommen ist:

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 } 

Der Fehler bleibt, auch wenn ich die explizite forall Syntax verwenden anstelle des :-> Typ-Operator.

Jetzt weiß ich, es gibt ein anderes Problem mit der "dämonischen Bindung", die Sie (>>) nicht definieren können, aber ich wollte immer noch sehen, wie weit ich damit gehen könnte. Kann irgendjemand erklären, warum ich GHC nicht dazu bringen kann, die "dämonische Bindung" zu entschlacken, selbst wenn es normalerweise Typ-check würde?

Answer 1

IIUC, der GHC desugarer läuft tatsächlich nach der Typchecker (source). Das erklärt, warum die von Ihnen beobachtete Situation theoretisch möglich ist. Der Typchecker hat wahrscheinlich einige spezielle Typisierungsregeln für die Do-Notation, und diese stimmen möglicherweise nicht mit dem überein, was der Typchecker mit dem entlädten Code machen würde.

Natürlich ist es vernünftig zu erwarten, dass sie konsistent sind, daher würde ich empfehlen, einen GHC-Fehler zu stellen.