obejmującego wszystkie przypadki promowanego typu danych

Question

Więc ja niedawno wpadł na ten zgrabny pomysł, w nadziei, że kod podziału między ścisłymi i leniwych modułów State transformatorowych:

{-# 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,()) 

Widać, że get i put Oba działają bez żadnego duplikowania - bez instancji klasy typu, bez niczego - zarówno na typach ścisłych, jak i leniwych. Jednak, mimo że obejmuje zarówno ewentualne przypadki dla Strictness, nie mam instancję monada dla State t s a ogólnie:

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

następujące prace w porządku, aczkolwiek wymagająca FlexibleContexts:

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

Potem można utworzyć instancję t pod numerem Lazy lub Strict i uruchomić wynik i uzyskać to, czego się spodziewam. Ale dlaczego muszę podać ten kontekst? Czy jest to ograniczenie koncepcyjne, czy praktyczne? Czy jest jakiś powód, dla którego brakuje mi tego, dlaczego Monad (State t s a) właściwie się nie trzyma, lub czy nie ma jeszcze sposobu, aby przekonać GHC o tym jeszcze?

(Na marginesie: przy użyciu kontekstu Monad (State t s)nie praca.

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

które po prostu myli mnie jeszcze bardziej pewnością były to wywnioskować z tego ostatniego?)

Answer 1

Jest to ograniczenie, ale jedno z ważnego powodu: gdyby nie działało w ten sposób, oczekiwane semantyka

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

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

dobrze, to może być

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 

lub może to być

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 

te nie są takie same. Jedną z możliwości byłoby zdefiniować funkcję dodatkową klasę, jak

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

a następnie następnie zdefiniować

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

i zamiast definiowania bindState jako część IsStrictness, można użyć pojedyncza

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

, które można jeszcze bardziej udoskonalić, korzystając z pojedynczej infrastruktury z GHC 7.6 zamiast niestandardowej klasy i typu singleton. Kończysz w ten sposób:

instance SingI t => Monad (State t s) 

co naprawdę nie jest takie straszne. Przyzwyczaić się do posiadania wielu SingI _ w zestawach ograniczeń. Tak to będzie działało przez jakiś czas i nie jest aż tak brzydkie.

Jako dlaczego State t [Bool] nie jest wywnioskować z State t s: problemem jest to, że State t s jest w górnym kontekście poziomu, co oznacza, że ​​s się ilościowo na poziomie peryferyjnych. Definiujesz funkcję, która mówi "dla każdego t i s takiego, że Monad (State t s) dam ci ...". Ale to nie mówi "dla każdego takiego, że Monad (stan [Bool]) dam ci ...". Niestety, te uniwersalnie wymierne ograniczenia nie są tak łatwe w Haskell.