제약 조건을 구체화하기 위해 Data.Constraint를 어떻게 사용합니까?

Question

나는 (MonadCo는 코 루틴 모나드를 대표하는 내 자신의 typeclass입니다. 당신이 좋아하는 경우. 문제는 동일합니다. 대신하는 경우 MonadError e m을 고려할 수) 유형

(forall m. (MonadCo r m, MonadReader Int m) => m()) 
    -> (forall m. (MonadCo r m, MonadReader Int m) => m()) 

의 기능이

이 보인다 내가 제약 조건을 구체화하고 형식 서명이있는 함수로 끝낼 수 있어야합니다.

(Equals k (MonadCo r, MonadReader Int)) 
    => (Constrain k()) -> (Constrain k()) 

그러나이 구현 방법에 대해서는 잘 모릅니다. 연습. 나는 :-과 :=>이 실제로 무엇인지에 대해 완전히 당혹 스럽다. 내가 을 어딘가에 필요로한다고 가정 해 보겠습니다. 왜냐하면 저는 보편적으로 m을 계량하고 있기 때문입니다.하지만 어디에 적합해야하는지 모르겠습니다.

실제로 내가하고자하는 일은 forall m. (MonadCo r m, MonadReader Int m) 제약을 구체화하는 것입니다. 나는 그 일을 할 때 왼편에 나타나는 모든 것이 자동적으로 "옳은 일"이라고 생각합니다.

Data.Constraint은 매우 강력하게 보이지만 어디에서 시작할 수 있습니까?

Answer 1

보이지 않습니다. 당신의 "Implies"가 k에서 반항적 인 것처럼 보이지만, 원하는 기능은 그렇지 않을 것입니다. ,

내 말은

, 당신은 어떤 기괴한 클래스 MonadFoo m이 있다면 무엇을, 당신은

type k m = (MonadCo r m, MonadReader Int m, MonadFoo m) 

이 클래스는 특별히 아니라 (이 클래스의 인스턴스가 하나만있을 수있는 방식으로 설계되어 있다고 가정 정의 GeneralizedNewtypeDeriving 이상을 사용하지 않는 경우), 일부 모나드 MMM은 MonadCo r 및 MonadReader Int의 인스턴스이기도합니다. 그렇다면 Constrain k() 유형은 아마도 MMM()과 동형 일 것입니다. 따라서, 함수를 원하는 경우 MMM() -> MMM() - 입력 유형이 MMM() 인 경우 함수가 작동하는 데 필요한 것보다 훨씬 약합니다. 이런 식으로 함수를 일반화 할 수는 없을 것입니다.

UPDATE :

일부 행복 Oleg'ing, 우리는 다음과 같은 코드가 있습니다

type ReaderAndCo r m = (MonadCo r m, MonadReader Int m) 

g :: (forall m . Dict (ReaderAndCo r m) -> m()) 
    -> (forall m . Dict (ReaderAndCo r m) -> m()) 
g x Dict = f (x Dict) 

당신은 분할을 촉진 할 수

{-# LANGUAGE ConstraintKinds #-} 
{-# LANGUAGE DefaultSignatures #-} 
{-# LANGUAGE FlexibleContexts #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE MultiParamTypeClasses #-} 
{-# LANGUAGE RankNTypes #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE TypeOperators #-} 
module Forall where 
import Control.Monad.Reader 
class Monad m => MonadCo r m where 
scary :: 
    (forall m. (MonadCo r m, MonadReader Int m) => m()) -> 
    (forall m. (MonadCo r m, MonadReader Int m) => m()) 
scary = undefined -- here goes your original function 
class Equals (d1 :: (* -> *) -> *) d2 where 
    equals :: p d2 -> p d1 
    default equals :: p d1 -> p d1 
    equals = id 
data Dict k (m :: * -> *) where Dict :: k m => Dict k m 
type Constraint d a = forall m. d m -> m a 
data (d1 :+: d2) (m :: * -> *) = Plus (d1 m) (d2 m) 
newtype ConstraintTrans d = ConstraintTrans {runCT :: Constraint d() -> Constraint d()} 
warmAndFuzzy :: 
    forall r d. 
    Equals d (Dict (MonadCo r) :+: Dict (MonadReader Int)) => 
    Constraint d() -> Constraint d() 
warmAndFuzzy = 
    let scary' :: 
      (MonadCo r m, MonadReader Int m) 
      => (forall m'. (MonadCo r m', MonadReader Int m') => m'()) 
       -> m() 
     scary' = scary 
     waf :: Constraint (Dict (MonadCo r) :+: Dict (MonadReader Int))() -> 
       Constraint (Dict (MonadCo r) :+: Dict (MonadReader Int))() 
     waf c (Plus Dict Dict) = 
      let arg :: forall m'. (MonadCo r m', MonadReader Int m') => m'() 
       arg = c $ Plus Dict Dict 
      in scary' arg 
    in runCT $ equals $ ConstraintTrans waf 

Answer 2

이것은 좋은 시작되어야한다 사전에 대한 ReaderAndCo 두 경우에 소원.

type Constrain k a = forall m . Dict (k m) -> m a 

g :: Constrain (ReaderAndCo r)() -> Constrain (ReaderAndCo r)() 
g x Dict = f (x Dict) 

이 당신이 달성하기 위해 원하는 것을가요 :

하면 추가 동의어를 도입 할 수 있습니다, 귀하의 질문의 코드에 더 유사한 만들려면?