Abdeckung aller Fälle eines geförderten Datentypen

Question

So vor kurzem ich mit dieser netten Idee kam, in der Hoffnung, des Teilen Code zwischen dem strengen und faul State Transformator Module:

{-# LANGUAGE FlexibleInstances, DataKinds, KindSignatures #-} 
module State where 

data Strictness = Strict | Lazy 
newtype State (t :: Strictness) s a = State (s -> (s, a)) 

returnState :: a -> State t s a 
returnState x = State $ \s -> (s, x) 

instance Monad (State Lazy s) where 
    return = returnState 
    State ma >>= amb = State $ \s -> case ma s of 
    ~(s', x) -> runState (amb x) s' 

instance Monad (State Strict s) where 
    return = returnState 
    State ma >>= amb = State $ \s -> case ma s of 
    (s', x) -> runState (amb x) s' 

get :: State t s s 
get = State $ \s -> (s, s) 

put :: s -> State t s() 
put s = State $ \_ -> (s,()) 

Sie können sehen, dass get und put Beide funktionieren ohne Duplizierung - keine Klasseninstanzen, nichts - sowohl bei den strikten als auch den faulen Typen. Ich

pro :: (Monad (State t [Bool])) => State t [Bool]() 
-- otherwise as before 

Dann: Doch obwohl ich beide möglichen Fälle für Strictness decken, ich habe keine Monade Instanz für State t s a im Allgemeinen:

-- from http://blog.melding-monads.com/2009/12/30/fun-with-the-lazy-state-monad/ 
pro :: State t [Bool]() 
pro = do 
    pro 
    s <- get 
    put (True : s) 

-- No instance for (Monad (State t [Bool])) arising from a do statement 

Folgende funktioniert gut, wenn auch erfordern FlexibleContexts kann t bei Lazy oder instanziieren und das Ergebnis ausführen und bekommen, was ich erwarte. Aber warum muss ich diesen Kontext geben? Ist das eine konzeptionelle oder praktische Einschränkung? Gibt es einen Grund, warum ich vermisse, warum Monad (State t s a) eigentlich nicht hält, oder gibt es einfach keine Möglichkeit, GHC davon zu überzeugen?

(abgesehen: den Kontext Monad (State t s)mit nicht Arbeit.

Could not deduce (Monad (State t [Bool])) arising from a do statement from the context (Monad (State t s))

, die nur noch mehr verwirrt mich Sicherlich ist der ehemalige ableitbar von letzterem?)

Answer 1

Dies ist eine Einschränkung, aber eine mit gutem Grund: Wenn es nicht so funktionierte, was würde die erwarteten Semantik von

runState :: State t s a -> s -> (s,a) 
runState (State f) s = f s 

example :: s -> a 
example = snd $ runState ((State undefined) >> return 1)() 

gut, könnte es

example = snd $ runState ((State undefined) >>= \_ -> return 1)() 
     = snd $ runState (State $ \s -> case undefined s of (s',_) -> (s',1))() 
     = snd $ case undefined() of (s',_) -> (s',1) 
     = snd $ case undefined of (s',_) -> (s',1) 
     = snd undefined 
     = undefined 

sein oder es könnte

example = snd $ runState ((State undefined) >>= \_ -> return 1)() 
     = snd $ runState (State $ \s -> case undefined s of ~(s',_) -> (s',1))() 
     = snd $ case undefined() of ~(s',_) -> (s',1) 
     = snd $ (undefined,1) 
     = 1 

diese sind nicht die gleichen sein. Eine Möglichkeit wäre, eine Funktion eine zusätzliche Klasse zu definieren, wie

class IsStrictness t where 
    bindState :: State t s a -> (a -> State t s b) -> State t s b 

und dann definieren Sie dann

instance IsStrictness t => Monad (State t s) where 
    return = returnState 
    (>>=) = bindState 

und stattdessen bindState als Teil IsStrictness definieren, können Sie einen Singleton verwenden

data SingStrictness (t :: Strictness) where 
    SingStrict :: SingStrictness Strict 
    SingLazy :: SingStrictness Lazy 

class IsStrictness t where 
    singStrictness :: SingStrictness t 

bindState :: IsStrictness t => State t s a -> (a -> State t s b) -> State t s b 
bindState ma' amb' = go singStrictness ma' amb' where 
    go :: SingStrictness t -> State t s a -> (a -> State t s b) -> State t s b 
    go SingStrict ma amb = ... 
    go SingLazy ma amb = ... 

, die mit den Singleton-Infrastruk- turen von GHC 7.6 anstelle der Custom Class- und Singleton-Typen noch weiter verbessert werden können. Sie werden sich mit

instance SingI t => Monad (State t s) 

beenden, die wirklich nicht so beängstigend ist. Gewöhnen Sie sich an viele SingI _ in Ihren Constraint-Sets. So wird es zumindest für eine Weile funktionieren und ist nicht so hässlich.

Wie, warum State t [Bool] ist nicht ableitbar aus State t s: Das Problem ist, dass State t s in Ihrem Top-Level-Kontext ist, was bedeutet, dass s an der äußersten Ebene quantifiziert. Du definierst eine Funktion, die sagt "für jedes t und s so, dass Monad (State t s) ich dir geben werde ...". Aber das sagt nicht "für so etwas wie Monad (Staat t [Bool]) werde ich Ihnen geben ...". Leider sind diese allgemein quantifizierten Einschränkungen in Haskell nicht so einfach.