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 头中不起作用。这一点也不奇怪，但似乎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

这个程序应该做什么？它不应该编译吗？如果不是，那么通过向一个类型添加一个构造函数，我们获取了一个您想要编译的程序，并生成了一个不需要编译的程序。如果它不应该编译，那么它有两个有效的行为。 

main = disp (DataTypeProxy :: DataTypeProxy 'Constructor)

只有一种可能的解释......但它需要您发送幻象类型。那是，

main = disp (DataTypeProxy :: DataTypeProxy 'SomethingElse)

是术语级别的相同程序，但具有不同的行为。这基本上打破了所有好的属性，比如参数化。基于类型类的调度是一个解决方案，因为范围内的实例以可预测的（和语义指定的）方式影响程序行为。

于 2012-06-13T03:07:26.757 回答