Do GADTs brechen equational Argumentation in Haskell

Question

Ich habe folgende Dolmetscher ProgramT aus dem operativen Paket

{-# LANGUAGE GADTs #-} 
import Control.Monad ((<=<)) 
import Control.Monad.Operational 

data Motor' a where 
    --Define GADT 

serialNewportT :: (Monad m, MonadIO m) => ProgramT Motor' m a -> m a 
serialNewportT = eval <=< viewT 
    where 
    eval :: (Monad m, MonadIO m) => ProgramViewT Motor' m v -> m v 
    eval (Return x) = return x 
    eval (x :>>= k) = f x >>= serialNewportT . k 

f :: (Monad m, MonadIO m) => Motor' a -> m a 
f = undefined -- excluded for brevity 

Der Code verwendet wird, wie es steht, zur Zeit überprüft geben Sie einfach in Ordnung. Ich möchte jedoch in der Lage sein, zu deaktivieren, wie der Interpreter verschiedene Motoren handhabt, also möchte ich f einen Parameter machen, anstatt ihn fest codieren zu lassen. Ich habe versucht, diesen Schalter mit dem folgenden Code

{-# LANGUAGE GADTs #-} 
import Control.Monad ((<=<)) 
import Control.Monad.Operational 

data Motor' a where 
    --Define GADT 

serialNewportT :: (Monad m, MonadIO m) => (Motor' a -> m a) -> ProgramT Motor' m a -> m a 
serialNewportT f = eval <=< viewT 
    where 
    eval :: (Monad m, MonadIO m) => ProgramViewT Motor' m v -> m v 
    eval (Return x) = return x 
    eval (x :>>= k) = f x >>= serialNewportT f . k 

zu machen

schlägt jedoch fehl, dieser Code mit einer Fehlermeldung

Couldn't match type ‘b’ with ‘c’ 
    ‘b’ is a rigid type variable bound by 
     a pattern with constructor 
     :>>= :: forall (instr :: * -> *) (m :: * -> *) a b. 
       instr b -> (b -> ProgramT instr m a) -> ProgramViewT instr m a, 
     in an equation for ‘eval’ 
    ‘c’ is a rigid type variable bound by 
     the type signature for 
     serialNewportT :: (Monad m, MonadIO m) => 
          (Motor' c -> m c) -> ProgramT Motor' m a -> m a 
Expected type: Motor' c 
    Actual type: Motor' b 

Da ich mit einem lokalen einem von der gleichen Art des globalen Namen bin nur zu ersetzen, hätte ich gedacht, dass es ohne Probleme gearbeitet haben soll. Wie kann ich die Typen mit f als Parameter vereinheitlichen?

Answer 1

Sie haben den Typ von f nicht korrekt übersetzt. Im ursprünglichen Code ist der Typ fforall a . (..) => Motor' a -> m a. Es könnte mit einer Art Motor' a für jedea, aber in der nicht-funktionierenden Code instanziiert werden feststellen, dass es Art ist genau das gleiche a wie in ProgramT Motor' m a, während in der Funktionskörper Sie f auf einem Motor' b für einige andere nennen (existentiell quantifiziert) Typ b.

Sie brauchen nur einen höheren Rang Typ:

serialNewportT :: (Monad m, MonadIO m) => (forall x . Motor' x -> m x) -> ProgramT Motor' m a -> m a