응용 프로그램 인스턴스 정의시의 문제점

Question

두 개의 유형 레벨 환경으로 색인 된 데이터 유형을 정의하려고한다고 가정하십시오. 같은 뭔가 :

data Woo s a = Woo a | Waa s a 

data Foo (s :: *) (env :: [(Symbol,*)]) (env' :: [(Symbol,*)]) (a :: *) = 
    Foo { runFoo :: s -> Sing env -> (Woo s a, Sing env') } 

아이디어는 env 입력 환경과 env' 출력 한 것입니다. 따라서 유형 Foo은 indexed state monad과 같은 역할을합니다. 여태까지는 그런대로 잘됐다. 제 문제는 어떻게 Foo이 신청자입니다. 명백한 시도는

instance Applicative (Foo s env env') where 
    pure x = Foo (\s env -> (Woo x, env)) 
    -- definition of (<*>) omitted. 

하지만 GHC는 완전히 합리적인 어떤 종류

pure :: a -> Foo s env env a 

대신 예상되는 형태

pure :: a -> Foo s env env' a 

을 유추하기 때문에 pure이 잘못 입력 된 것을 뿌려줍니다. 요점은, Foo에 대한 Applicative 인스턴스를 정의하여 환경 유형을 변경할 수 있습니까? 나는 indexed functors를 googled했다. 그러나 처음에, 그들은 나의 문제를 해결하는 것처럼 보이지 않는다. 누군가 이것을 달성하기 위해 뭔가를 제안 할 수 있습니까?

Answer 1

귀하의 Foo 유형은 Atkey는 원래 parameterised monad라는 내용의 예이고, 다른 사람은 (틀림없이 잘못) 지금 색인 모나드를 호출합니다.

인덱싱 된 모나드는 유형의 방향 그래프를 통해 경로를 설명하는 두 개의 인덱스가있는 모나드 형 오브젝트입니다. 인덱싱 된 모나드 계산을 시퀀싱하려면 두 계산의 인덱스가 도미노처럼 정렬되어 있어야합니다. 당신이 y에서 z에 도착하는 x에서 y의 경로를 설명하는 인덱스 모나드 및 방법이있는 경우

class IFunctor f where 
    imap :: (a -> b) -> f x y a -> f x y b 

class IFunctor f => IApplicative f where 
    ipure :: a -> f x x a 
    (<**>) :: f x y (a -> b) -> f y z a -> f x z b 

class IApplicative m => IMonad m where 
    (>>>=) :: m x y a -> (a -> m y z b) -> m x z b 

는 인덱스 바인드 >>>= 당신에게 x에서 z로 이동 더 큰 계산을 제공 할 것입니다.

또한 ipure은 f x x a을 반환합니다. ipure에 의해 반환 된 값은 유형의 유향 그래프를 통해 어떠한 단계도 수행하지 않습니다. 유형 수준 id과 같습니다.

색인 모나드의 간단한 예는, 어떤 당신이 당신의 질문에 언급하기 i에서 o에 대한 인수의 형식을 변환하는 인덱스 상태 모나드 newtype IState i o a = IState (i -> (o, a))입니다. 첫 번째 출력 유형이 두 번째 입력 유형과 일치하는 경우에만 상태 저장 연산을 시퀀싱 할 수 있습니다. 실제 질문에 이제

---

newtype IState i o a = IState { runIState :: i -> (o, a) } 

instance IFunctor IState where 
    imap f s = IState $ \i -> 
     let (o, x) = runIState s i 
     in (o, f x) 

instance IApplicative IState where 
    ipure x = IState $ \s -> (s, x) 
    sf <**> sx = IState $ \i -> 
     let (s, f) = runIState sf i 
      (o, x) = runIState sx s 
     in (o, f x) 

instance IMonad IState where 
    s >>>= f = IState $ \i -> 
     let (t, x) = runIState s i 
     in runIState (f x) t 

. domino-esque 시퀀싱을 사용하는 IMonad은 유형 수준 환경을 변환하는 계산을위한 좋은 추상화입니다. 첫 번째 계산이 환경을 두 번째 상태에 알맞은 상태로 유지할 것으로 기대합니다. Foo에 IMonad의 인스턴스를 작성하겠습니다.

Woo s a 유형이 Writer 모나드의 예인 (a, Maybe s)과 같은 모양이라는 점부터 알아 보겠습니다. 우리가 나중에 Monad (Woo s)에 대한 인스턴스를 필요로하기 때문에 나는 이것을 언급하고 나 자신을 쓰기에는 너무 게으른 편이다.

type Woo s a = Writer (First s) a 

내가 Maybe 모노 이드의 내 선호하는 맛으로 First을 골랐다하지만 Woo를 사용하려면 어떻게 정확히 알 수 없습니다. Last을 선호 할 수도 있습니다.

또한 Writer이 Traversable의 인스턴스라는 사실을 곧 사용할 예정입니다. 실제로 Writer은 그 이상으로 이동하기가 쉽습니다. 정확히 하나의 a이 포함되어 있기 때문에 어떤 결과도 함께 제거 할 필요가 없습니다. 즉, 효과가있는 f에 대해 Functor 제약 조건 만 있으면됩니다.

-- cf. traverse :: Applicative f => (a -> f b) -> t a -> f (t b) 
traverseW :: Functor f => (a -> f b) -> Writer w a -> f (Writer w b) 
traverseW f m = let (x, w) = runWriter m 
       in fmap (\x -> writer (x, w)) (f x) 

사업에 착수합시다.

Foo s은 IFunctor입니다. 이 인스턴스는 Writer s의 functor-ness를 사용합니다 : 우리는 stateful 계산을하고 fmapWriter 모나드 함수를 사용합니다.

newtype Foo (s :: *) (env :: [(Symbol,*)]) (env' :: [(Symbol,*)]) (a :: *) = 
    Foo { runFoo :: s -> Sing env -> (Woo s a, Sing env') } 

instance IFunctor (Foo s) where 
    imap f foo = Foo $ \s env -> 
     let (woo, env') = runFoo foo s env 
     in (fmap f woo, env') 

우리는 또한 나중에 traverseW와 함께 사용, 일반 FunctorFoo를 확인해야합니다.

instance Functor (Foo s x y) where 
    fmap = imap 

Foo s는 IApplicative입니다. Woo을 함께 분쇄하려면 Writer s의 Applicative 인스턴스를 사용해야합니다. 이 부분은 Monoid s 제약 조건에서 비롯됩니다.

instance IApplicative (Foo s) where 
    ipure x = Foo $ \s env -> (pure x, env) 
    foo <**> bar = Foo $ \s env -> 
     let (woof, env') = runFoo foo s env 
      (woox, env'') = runFoo bar s env' 
     in (woof <*> woox, env'') 

Foo s는 IMonad입니다. 놀람 놀람, 우리는 Writer s의 Monad 인스턴스에 위임하는 것을 끝낸다. 작가 안의 중간에 a을 먹이기 위해 traverseW을 교묘히 사용하는 것은 클레이슬러 화살표 f에 유의하십시오.

instance IMonad (Foo s) where 
    foo >>>= f = Foo $ \s env -> 
     let (woo, env') = runFoo foo s env 
      (woowoo, env'') = runFoo (traverseW f woo) s env' 
     in (join woowoo, env'') 

---

부록 :이 그림에서 빠진 것은 변압기입니다.

type Foo s env env' = ReaderT s (IStateT (Sing env) (Sing env') (WriterT (First s) Identity)) 

을하지만 인덱스 모나드는 변압기에 대해 사람들에게 꼭 이야기를하지 않습니다 본능은 당신이 모나드 변압기 스택으로 Foo을 표현 할 수 있어야한다고 하더군요. >>>=의 타입은 스택의 모든 인덱스 된 모나드가 같은 방식으로 인덱스를 조작해야 할 필요가 있습니다. 이것은 아마도 원하는 것이 아닙니다. 인덱싱 된 모나드는 일반 모나드와도 잘 어울리지 않습니다.

이 모든 것은 인덱스 된 모나드 변환기가 McBride-style indexing scheme으로 조금 더 멋지게 재생된다는 것을 말합니다. 맥브라이드의 IMonad은 다음과 같습니다

type f ~> g = forall x. f x -> g x 

class IMonad m where 
    ireturn :: a ~> m a 
    (=<?) :: (a ~> m b) -> (m a ~> m b) 

그리고 모나드 변압기는 다음과 같이 보일 것이다 :

class IMonadTrans t where 
    ilift :: IMonad m => m a ~> t m a 

Answer 2

기본적으로, 당신은 Sing env'에 제약을 놓치고있어 - 그것은 Monoid 할 필요가 즉 것을, 때문에 : 당신은 아무것도에서 유형 Sing env'의 값을 생성 할 수 있어야합니다

• (예 mempty를)
• <*> (예 : mappend) 동안 Sing env' 유형의 두 값을 하나로 결합 할 수 있어야합니다. 당신이 어딘가에에서 SemiGroup를 가져올하지 않는

는 또한 당신은이 너무 Monoid되고 싶어 아마 것, <*>에 s 값을 결합 능력을 필요로하므로 것이다.

{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE FlexibleContexts #-} 
{-# LANGUAGE DeriveFunctor #-} 
module SO37860911 where 
import GHC.TypeLits (Symbol) 
import Data.Singletons (Sing) 

data Woo s a = Woo a | Waa s a 
    deriving Functor 

instance Monoid s => Applicative (Woo s) where 
    pure = Woo 
    Woo f <*> Woo a = Woo $ f a 
    Waa s f <*> Woo a = Waa s $ f a 
    Woo f <*> Waa s a = Waa s $ f a 
    Waa s f <*> Waa s' a = Waa (mappend s s') $ f a 

data Foo (s :: *) (env :: [(Symbol,*)]) (env' :: [(Symbol,*)]) (a :: *) = 
    Foo { runFoo :: s -> Sing env -> (Woo s a, Sing env') } 
    deriving Functor 

instance (Monoid s, Monoid (Sing env')) => Applicative (Foo s env env') where 
    pure a = Foo $ \_s _env -> (pure a, mempty) 
    Foo mf <*> Foo ma = Foo $ \s env -> case (mf s env, ma s env) of 
    ((w,e), (w',e')) -> (w <*> w', e `mappend` e')