4

昇格されたデータ型には、昇格されたデータの種類のメンバーである固定数の型があります。この閉ざされた世界では、明示的にスコープ内にある辞書なしで、型クラスで関数の呼び出しをサポートすることは理にかなっていますか?

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}

data DataType = Constructor

data DataTypeProxy (e :: DataType) = DataTypeProxy

class Class (e :: DataType) where
  classFunction :: DataTypeProxy e -> IO ()

-- this is the only instance that can be created
instance Class 'Constructor where
  classFunction _ = return ()

-- adding the Class constraint fixes the build break
-- disp :: Class e => DataTypeProxy e -> IO ()
disp :: DataTypeProxy e -> IO ()
disp = classFunction

main :: IO ()
main = disp (DataTypeProxy :: DataTypeProxy 'Constructor)

この不自然な例は、GHC head では機能しません。まったく驚くべきことではありませんが、DataKind拡張機能によってこれが可能になるようです。

test.hs:18:8:
    No instance for (Class e) arising from a use of `classFunction'
    Possible fix:
      add (Class e) to the context of
        the type signature for disp :: DataTypeProxy e -> IO ()
    In the expression: classFunction
    In an equation for `disp': disp = classFunction
4

1 に答える 1

4

いいえ。それを許可すると、ファントム データ型は実行時に追加の型情報で「タグ付け」する必要があり、あいまいさが生じます。 

data DataType = Constructor | SomethingElse

data DataTypeProxy (e :: DataType) = DataTypeProxy 
...
instance Class 'SomethingElse where
   classFunction _ = putStrLn "hello world"

instance Class 'Constructor where
   classFunction _ = return ()

disp :: DataTypeProxy e -> IO ()
disp = classFunction

main = disp DataTypeProxy

このプログラムは何をすべきですか？コンパイルしないでください。そうでない場合は、型にコンストラクターを追加することで、コンパイルしたいプログラムを取得し、コンパイルしないプログラムを作成しました。コンパイルできない場合は、2 つの有効な動作があります。 

main = disp (DataTypeProxy :: DataTypeProxy 'Constructor)

可能な解釈は 1 つだけです...しかし、ファントム タイプでディスパッチする必要があります。あれは、

main = disp (DataTypeProxy :: DataTypeProxy 'SomethingElse)

用語レベルでは同一のプログラムですが、動作が異なります。それは基本的に、パラメトリックのようなすべての優れたプロパティを壊します。型クラスベースのディスパッチは、これに対する解決策です。スコープ内のどのインスタンスが、予測可能な (そして意味論的に指定された) 方法でプログラムの動作に影響を与えるからです。

于 2012-06-13T03:07:26.757 に答える