が促進データ型

Question

のすべてのケースをカバーだから私は最近、厳しいと怠惰Stateトランスモジュール間の共有コードの希望で、このきちんとしたアイデアを思い付いた：

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

あなたはそのgetとputを見ることができますどちらも重複なしに動作します。厳密な型と遅延型の両方で、型クラスインスタンスはなく、何もありません。しかし、私はStrictnessのための可能なケースの両方をカバーするにもかかわらず、私は一般的にState t s aためモナドのインスタンスを持っていない：

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

次はFlexibleContextsを必要とするにもかかわらず、正常に動作します：

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

次にI tをLazyまたはStrictにインスタンス化して結果を実行し、私が期待するものを得ることができます。しかし、なぜ私はそのコンテキストを与えなければならないのですか？これは概念的な限界か、それとも実用的なものですか？ Monad (State t s a)が実際に保持しない理由が何か不足していますか、それともGHCをまだ納得させる方法がありませんか？

（脇：コンテキストにMonad (State t s)を使用して仕事しません：。

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

だけでも、より多くの私を混乱させる確かに前者が後者から演繹あります？）

Answer 1

これは限られていますが、理由があります：もしうまくいかないとすればうまく

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

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

の予想セマンティクスが、それは

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 

か、それはこれらが同じではない

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 

可能性がある可能性があります。その後、

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

を定義し、代わりにIsStrictnessの一部としてbindStateを定義するので、あなたがシングルトンを使用することができます1つのオプションは、その後

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

と同様に、機能に余分なクラスを定義することです

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

これはカスタムクラスとシングルトンタイプの代わりにGHC 7.6のシングルトンインフラストラクチャを使用してさらに強化することができます。あなたは

instance SingI t => Monad (State t s) 

となりますが、これは本当に恐ろしいことではありません。あなたの制約セットに多くのSingI _を持つことに慣れてください。これは、それが少なくともしばらくの間働く方法であり、それほど醜いものではありません。問題はState t sがsは、最も外側のレベルで定量化されることを意味し、あなたのトップレベルの文脈であるということである：State t [Bool]はState t sから演繹ない理由として

。あなたは "Monad（State t s）があなたに与えるようなtとsのために..."と言う関数を定義しています。しかし、これは「モナド（国家[ブール]）が私にあなたを与えるようなものはない」とは言わない。悲しいことに、これらの普遍的に定量化された制約は、Haskellではあまり簡単ではありません。