如何使用Data.Constraint來約化約束？

我有型如何使用Data.Constraint來約化約束？

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

的功能（MonadCo是代表協程單子我自己的類型類。如果你喜歡，你可以考慮的情況下MonadError e m來代替。這個問題將是相同的。）

似乎像我應該能夠具體化的約束，並與像

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

與簽名類型的函數結束了，但我不知道如何去執行這一實踐。我完全不知道:-和:=>究竟是什麼。我想我也需要一個Forall1在那裏，因爲我普遍量化m，但我不知道它應該在哪裏。

真的我想要做的是通過forall m. (MonadCo r m, MonadReader Int m)約束。我認爲，當我這樣做的時候，無論結果出現在左邊什麼都會自動成爲「正確的事情」。

Data.Constraint看起來非常強大，但我無法確定從哪裏開始。

來源

2014-01-21 Tom Ellis

這當然有可能。而且你不需要像'：'或'Forall1'這樣的可怕東西。 – MigMit

似乎不可能。看起來你的「意味着」在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，我們有以下代碼：

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

來源

2014-01-21 17:36:04 MigMit

好的，我明白你的意思是關於反轉。我會編輯這個問題，以減少不可能的事情。但我真的不是在問一個確切的問題。相反，我在問如何確定約束條件，我的例子實際上只是我最近關於它應該是什麼樣子的混淆思想。 –

哇。我現在實際上認爲你關於逆變的原始評論對我來說是關鍵，並且讓我意識到我原本試圖達到的目標可能是不可能的。那謝謝啦！ –

這應該是一個良好的開端：

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)

可以進一步拆分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)

這是你想要達到什麼樣的？

來源

2014-01-21 18:14:02

我們還可以添加class Equals k1 k2，其中等於:: p k1 - > p k2（帶有某些類型的簽名）。 – MigMit

我認爲這讓我意識到，我試圖達到的最終結果實際上是不可能的，這非常有用，所以謝謝！ –

如何使用Data.Constraint來約化約束？

回答

相關問題