2

GADTとDataKindsを使用して発生している問題の非常に単純な例を作成しました。私の実際のアプリケーションは明らかにより複雑ですが、これは私の状況の本質を明確に捉えています。Test型の任意の値（T1、T2）を返すことができる関数を作成しようとしています。これを達成する方法はありますか、それとも依存型の領域に入りますか？ここでの質問は似ているように見えますが、私はそれらから私の質問に対する答えを見つけることができませんでした（または理解できませんでした）。私はこれらのGHC拡張機能を理解し始めたばかりです。ありがとう。

同様の質問1

同様の質問2

{-# LANGUAGE GADTs, DataKinds, FlexibleInstances, KindSignatures #-}

module Test where

data TIdx = TI | TD

data Test :: TIdx -> * where
  T1 :: Int -> Test TI
  T2 :: Double -> Test TD

type T1 = Test TI
type T2 = Test TD

prob :: T1 -> T2 -> Test TIdx
prob x y = undefined

----ここにエラーがあります----Test.hs：14：26：

Kind mis-match

The first argument of `Test' should have kind `TIdx',

but `TIdx' has kind `*'

In the type signature for `prob': prob :: T1 -> T2 -> Test TIdx
4

2 に答える 2

6

表示されるエラー メッセージは、型パラメーター toTestに kind が必要なためですTIdxが、その種類を持つ型はTIandだけTDです。type TIdxには kind があります*。

あなたが表現しようとしていることを正しく理解していれば、 の結果の型はprobまたはTest TIですTest TDが、実際の型は実行時に決定されます。ただし、これは直接には機能しません。通常、戻り値の型はコンパイル時にわかっている必要があります。

GADT コンストラクターはそれぞれ kind の特定の phatom タイプにマップされるため、できることはTIdx、存在する GADT または別の GADT でファントム タイプを消去し、後でパターン マッチを使用してタイプを回復する結果を返すことです。

たとえば、特定の種類の を必要とする 2 つの関数を定義するとしますTest。

fun1 :: T1 -> IO ()
fun1 (T1 i) = putStrLn $ "T1 " ++ show i

fun2 :: T2 -> IO ()
fun2 (T2 d) = putStrLn $ "T2 " ++ show d

この型チェック:

data UnknownTest where
    UnknownTest :: Test t -> UnknownTest

prob :: T1 -> T2 -> UnknownTest
prob x y = undefined

main :: IO ()
main = do
    let a = T1 5
        b = T2 10.0
        p = prob a b

    case p of
        UnknownTest t@(T1 _) -> fun1 t
        UnknownTest t@(T2 _) -> fun2 t

ここで注目すべきことは、case-expression では、 UnknownTestGADT がファントム型を消去したとしても、コンストラクターT1とT2コンストラクターが十分な型情報をコンパイラーに提供し、正確な型または case-expression の分岐内をt回復することです。これらの特定の型を期待する関数を呼び出します。Test TITest TD

于 2013-02-17T08:20:14.380 に答える
1

ここには2つのオプションがあります。引数の型から戻り値の型を推測できるか、推測できないかのどちらかです。

前者の場合、タイプを改良します。

data Which :: TIdx -> * where
  Fst :: Which TI
  Snd :: Which TD

prob :: Which i -> T1 -> T2 -> Test i
prob Fst x y = x
prob Snd x y = y

後者の場合、タイプ情報を消去する必要があります。

prob :: Bool -> T1 -> T2 -> Either Int Double
prob True (T1 x) y = Left x
prob False x (T2 y) = Right y

実存型を使用して、型情報を消去することもできます。

data SomeTest = forall i . SomeTest (Test i)

prob :: Bool -> T1 -> T2 -> SomeTest
prob True x y = SomeTest x
prob False x y = SomeTest y

この場合、値を使用して面白いことを行うことはできませんがSomeTest、実際の例ではできる可能性があります。

于 2013-02-17T07:48:49.210 に答える