haskell - 再帰型ファミリー

Question

私は、外側のモナドの上に構図mtlを持ち上げることができるスタイルのクラスを試しています。Pipeそのためには、タイプのどの2つの変数がPipe構成の定義域と終域であるかを定義する必要があります。

私は関連する型族のアプローチを使用しようとしましたが、役に立ちませんでした：

{-# LANGUAGE TypeFamilies #-}

import Control.Monad.Trans.Free
import Control.Monad.Trans.State
import Control.Pipe hiding (Pipe)

data Pipe a b m r = Pipe { unPipe :: FreeT (PipeF a b) m r }

class MonadPipe m where
    type C a b (m :: * -> *) :: * -> *
    idT :: C a a m r
    (<-<) :: C b c m r -> C a b m r -> C a c m r

instance (Monad m) => MonadPipe (Pipe i o m) where
    type C a b (Pipe i o m) = Pipe a b m
    idT = Pipe idP
    (Pipe p1) <-< (Pipe p2) = Pipe (p1 <+< p2)

instance (MonadPipe m) => MonadPipe (StateT s m) where
    type C a b (StateT s m) = StateT s (C a b m)
    idT = StateT $ \s -> idT
    (StateT f1) <-< (StateT f2) = StateT $ \s -> f1 s <-< f2 s

ただし、上記のコードは型チェックを行いません。GHCは次のエラーを出します：

family.hs:23:15:
    Could not deduce (C a a m ~ C a0 a0 m0)
    from the context (MonadPipe m)
      bound by the instance declaration at family.hs:21:14-52
    NB: `C' is a type function, and may not be injective
    Expected type: C a a (StateT s m) r
      Actual type: StateT s (C a0 a0 m0) r
    In the expression: StateT $ \ s -> idT
    In an equation for `idT': idT = StateT $ \ s -> idT
    In the instance declaration for `MonadPipe (StateT s m)'

family.hs:24:10:
    Could not deduce (C b c m ~ C b0 c0 m1)
    from the context (MonadPipe m)
      bound by the instance declaration at family.hs:21:14-52
    NB: `C' is a type function, and may not be injective
    Expected type: C b c (StateT s m) r
      Actual type: StateT s (C b0 c0 m1) r
    In the pattern: StateT f1
    In an equation for `<-<':
        (StateT f1) <-< (StateT f2) = StateT $ \ s -> f1 s <-< f2 s
    In the instance declaration for `MonadPipe (StateT s m)'

<<Two other errors for 'C a b m' and 'C a c m'>>

特に定義に関して、型が統一されない理由を理解するのは難しいですidT。なぜなら、内側idTが全称記号で表されa、外側の型と一致することを期待しているからです。

だから私の質問は、これが型族で実装可能かどうか、そして型族で不可能な場合、どのように実装できるかということです。

score 12 · Accepted Answer

型推論は、デフォルトでは推測ゲームです。forallHaskell の表面構文では、必要なものがわかっている場合でも、どの型でをインスタンス化する必要があるかを明示するのはかなり厄介です。これは、Damas-Milner の完全性の古き良き時代からの遺産です。当時は、明示的な型付けを必要とするほど興味深いアイデアは単純に禁止されていました。

f {a = x}Agda スタイルの表記法を使用してパターンと式でa型適用を明示的にすることが許可されていると想像してみましょうf。君の

idT = StateT $ \ s -> idT

意味するはずです

idT {a = a}{m = m} = StateT $ \ s -> idT {a = a}{m = m}

左側には type がC a a (StateT s m) rあり、右側には typeStateT s (C a a m) rがあり、これらは型ファミリーの定義によって等しくなり、世界中に喜びが広がります。しかし、それはあなたが書いたことの意味ではありません。ポリモーフィックなものを呼び出すための「変数ルール」では、それぞれforallが新しい存在型変数でインスタンス化され、統合によって解決される必要があります。したがって、コードの意味は

idT {a = a}{m = m} = StateT $ \ s -> idT {a = a'}{m = m'}
  -- for a suitably chosen a', m'

型ファミリを計算した後に利用可能な制約は次のとおりです。

C a a m ~ C a' a' m'

Cしかし、それは単射であると仮定する理由がないため、単純化する必要はありません。そして驚くべきことは、最も一般的な解を見つける可能性について、マシンがあなたよりも気にかけているということです。あなたはすでに適切な解決策を考えていますが、問題は、デフォルトの仮定が当て推量である場合にコミュニケーションを達成することです。

このジャムから抜け出すのに役立つ戦略がいくつかあります。1 つは、代わりにデータファミリを使用することです。長所: 単射性は問題ありません。短所：コンストラクタ。（警告、以下のテストされていない推測。）

class MonadPipe m where
  data C a b (m :: * -> *) r
  idT :: C a a m r
  (<-<) :: C b c m r -> C a b m r -> C a c m r

instance (MonadPipe m) => MonadPipe (StateT s m) where
  data C a b (StateT s m) r = StateTPipe (StateT s (C a b m) r)
  idT = StateTPipe . StateT $ \ s -> idT
  StateTPipe (StateT f) <-< StateTPipe (StateT g) =
    StateTPipe . StateT $ \ s - f s <-< g s

もう 1 つの短所は、結果として得られるデータファミリが自動的にモナドにならないことです。また、それをアンラップしたり、均一な方法でモナドにしたりするのも非常に簡単ではありません。

タイプファミリーを維持しながら、そのための newtype ラッパーを定義するパターンを試してみることを考えています。

newtype WrapC a b m r = WrapC {unwrapC :: C a b m r}

次にWrapC、操作の型で使用して、型チェッカーを正しい軌道に乗せます。それが良い戦略かどうかはわかりませんが、いつか見つけようと思っています。

より直接的な戦略は、プロキシ、ファントム型、およびスコープ型変数を使用することです (ただし、この例では必要ありません)。（繰り返しますが、憶測警告です。）

data Proxy (a :: *) = Poxy
data ProxyF (a :: * -> *) = PoxyF

class MonadPipe m where
  data C a b (m :: * -> *) r
  idT :: (Proxy a, ProxyF m) -> C a a m r
  ...

instance (MonadPipe m) => MonadPipe (StateT s m) where
  data C a b (StateT s m) r = StateTPipe (StateT s (C a b m) r)
  idT pp = StateTPipe . StateT $ \ s -> idT pp

これは、型適用を明示的にするための厄介な方法です。一部の人々は引数としてand を渡すa代わりにそれ自身を使用することに注意してください。に関する最近の進歩は、少なくとも 1 種類の多態性ファントムプロキシタイプを持つことができることを意味する可能性があります。重要なことに、型コンストラクターは単射であるため、私のコードは実際には「ここと同じパラメーター」と言っています。Proxy aundefinedPolyKindsProxy

しかし、ソースコードでシステム FC レベルに落とし込みたい場合や、型推論のために明確な手動オーバーライドを表現したい場合があります。このようなことは、依存型付けされたコミュニティでは非常に標準的です。そこでは、マシンがあちこちで微調整しなくてもすべてを理解できる、または隠された引数に検査する価値のある情報が含まれていないなどとは誰も想像していません。関数への隠し引数を使用箇所で抑制できるが、定義内で明示的にする必要があることはよくあることです。Haskell の現在の状況は、「型推論で十分」という文化的前提に基づいています。これは、何世代にもわたって軌道に乗っていませんでしたが、依然として何とか存続しています。

score 4 · Accepted Answer

編集済み 3 回: データファミリのバージョンについては下部を参照してください。また、GADT のバージョンをドロップ m に変更しました。

推測させてください：残り物？

最初に型エラー、a SOLUTION について説明します。

The class defines :
type C a0 b0 m  where a0 and b0 are fresh.
idT :: C a a m r, where a and r are fresh. 

The idT in the (Pipe i o m0) instance is okay by what I think is the logic:
LHS is idT :: C a0 a0 (Pipe i o m0) r0 which becomes Pipe a0 a0 m0 r0
RHS is Pipe idP :: Pipe a1 a1 m1 r1 starts fresh
And then these unify
because Pipe is a data constructor.

The idT in the MonadPipe m0 => (StateT s0 m0) instance:
LHS is idT :: C a0 a0 (StateT s0 m0) which becomes StateT s0 (C a0 a0 m0)
RHS is StateT (\s -> idT) :: StateT s1 m1 r1
Some unification seems to happen...
RHS is StateT (\s -> idT) :: StateT s1 (C a0 a0 m0) r1
  where expression idT :: MonadPipe m1 => (C a2 a2 m2) r2 starts fresh
        context of idT :: (C a0 a0 m0) (a1, s1)
And then (C a0 a0 m0) does not unify with (C a1 a2 m2)
because C is a type constructor.

newtype型ファミリがデータファミリになる場合、Category インスタンスを作成する以前の方法はおそらくここで機能します。

編集: パラメータの順序を変更し、それを解決するには newtype StateT を使用します。

{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}

import Control.Monad.Trans.Free
import Control.Monad.Trans.State
import Control.Pipe hiding (Pipe)

data Pipe m a b r = Pipe { unPipe :: FreeT (PipeF a b) m r }

newtype StatePipe s mp a b r = SP (StateT s (mp a b) r)

class MonadPipe mp where
    idT :: mp a a r
    (<-<) :: mp b c r -> mp a b r -> mp a c r

instance (Monad m) => MonadPipe (Pipe m) where
    idT = Pipe idP
    (Pipe p1) <-< (Pipe p2) = Pipe (p1 <+< p2)

instance (MonadPipe mp) => MonadPipe (StatePipe s mp) where
     idT = SP . StateT $ \s -> idT
     (SP (StateT f1)) <-< (SP (StateT f2)) = SP . StateT $ \s -> f1 s <-< f2 s

MonadTrans は悲しいかもしれませんが。別のアプローチでは、GADT を使用して引数の順序を維持し、構築しようとしているものをより明確に表現します。

{-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleInstances #-}
import Control.Monad.Trans.Free
import Control.Monad.Trans.State
import Control.Pipe hiding (Pipe)

data Pipe s a b m r where
  FPipe :: { unPipe :: FreeT (PipeF a b) m r } -> Pipe () a b m r
  LPipe :: StateT s1 (Pipe s2 a b m) r -> Pipe (s1,s2) a b m r

class MonadPipe s where
    idT :: Monad m => Pipe s a a m r
    (<-<) :: Monad m => Pipe s b c m r -> Pipe s a b m r -> Pipe s a c m r

instance MonadPipe () where
    idT  = FPipe idP
    (FPipe p1) <-< (FPipe p2) = FPipe (p1 <+< p2)

instance MonadPipe s2 => MonadPipe (s1,s2) where
    idT  = LPipe (StateT $ \s -> idT)
    (LPipe (StateT f1)) <-< (LPipe (StateT f2)) = 
       LPipe (StateT $ \s1 -> (f1 s1 <-< f2 s1))

そして、これをおそらくさらに優れたデータファミリに変換できますか?

{-# LANGUAGE TypeFamilies #-}
import Control.Monad.Trans.Free
import Control.Monad.Trans.State
import Control.Pipe hiding (Pipe)

data family GPipe s :: * -> * -> (* -> *) -> * -> *
newtype instance GPipe () a b m r = Pipe { unPipe :: FreeT (PipeF a b) m r }
newtype instance GPipe (s1,s2) a b m r = LPipe ( StateT s1 (GPipe s2 a b m) r )

class MonadPipe s where
  idT :: Monad m => GPipe s a a m r
  (<-<) :: Monad m => GPipe s b c m r -> GPipe s a b m r -> GPipe s a c m r

instance MonadPipe () where
  idT = Pipe idP
  (Pipe p1) <-< (Pipe p2) = Pipe (p1 <+< p2)

instance MonadPipe s2 => MonadPipe (s1,s2) where
  idT = LPipe (StateT (\s -> idT))
  (LPipe (StateT f1)) <-< (LPipe (StateT f2)) = LPipe (StateT (\s -> f1 s <-< f2 s))

haskell - 再帰型ファミリー

2 に答える 2

Related

Reference