複数のコンストラクタから最も一般的な型を抽出する

Question

以下のコードでは、関数fのアイデアは妥当であると確信しています。最初の要素の型がわからないのはDですが、T aいくつかはaです。

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE RankNTypes #-} 

data T a 

data D where 
    D1 :: T a -> D 
    D2 :: T Bool -> D 

f :: D -> (forall a. T a) 
f (D1 x) = x 
f (D2 x) = x 

main = return() 

ただし、GHCは、次のエラーがスローされます。

GADTTypes.hs:11:12: error: 
    • Couldn't match type ‘a1’ with ‘a’ 
     ‘a1’ is a rigid type variable bound by 
     a pattern with constructor: D1 :: forall a. T a -> D, 
     in an equation for ‘f’ 
     at GADTTypes.hs:11:4 
     ‘a’ is a rigid type variable bound by 
     the type signature for: 
      f :: forall a. D -> T a 
     at GADTTypes.hs:11:1 
     Expected type: T a 
     Actual type: T a1 
    • In the expression: x 
     In an equation for ‘f’: f (D1 x) = x 
    • Relevant bindings include x :: T a1 (bound at GADTTypes.hs:11:7) 
GADTTypes.hs:12:12: error: 
    • Couldn't match type ‘a’ with ‘Bool’ 
     ‘a’ is a rigid type variable bound by 
     the type signature for: 
      f :: forall a. D -> T a 
     at GADTTypes.hs:11:1 
     Expected type: T a 
     Actual type: T Bool 
    • In the expression: x 
     In an equation for ‘f’: f (D2 x) = x 

ただ、私が達成しようとしていることは可能であるかどうかを疑問に、どのように自分のコードを修正するには？

Answer 1

ハスケルにはexists a. T aがありませんが、これはあなた自身のタイプを宣言することができます。あなたは

g :: T a -> ... 

を持っていて、g (f x)を構成する場合

data T a 

data D where 
    D1 :: T a -> D 
    D2 :: T Bool -> D 

data ExT where 
    ExT :: T a -> ExT 

f :: D -> ExT 
f (D1 x) = ExT x 
f (D2 x) = ExT x 

次に、あなたの代わりに

case f x of 
    ExT y -> g y 

注意を使用する必要があることを明らかに同等以下のコードでしょうない型チェック代わりに（existsタイプがないため）。あなたが望むなら

g (case f x of 
    ExT y -> y) 

あなたはそのために、独自のヘルパーを作ることができます。

help :: (forall a. T a -> b) -> ExT -> b 
help h (ExT x) = h x 

-- example 
foo x = help g (f x) 

これは近い平野g (f x)の構文を続けるだろう。

Answer 2

あなたの署名は、すべてaのためにT aを返すと主張しています。私はあなたにD2を渡し、T Intを求める場合しかし、あなたはあなたの署名が嘘をついているので、それを提供することができないでしょう。

）私はあなたがここにexistsとしてforallを誤って解釈していると思います。存在タイプは、Haskell Wikiに示すように、Universalタイプ（forall）でも実装できます。