功能类型的种类 [英] Kinds of types in functions

问题描述

使用以下代码：

  { - ＃LANGUAGE KindSignatures，DataKinds＃ - } 
 
数据Nat = O | S Nat 
 
 class NatToInt（n :: Nat）其中
 natToInt :: n  - > Int 
 
实例NatToInt O其中
 natToInt _ = 0 
 
实例（NatToInt n）=> NatToInt（S n）其中
 natToInt _ = 1 + natToInt（undefined :: n）
  

GHC通知我们它期望 natToInt 类型规范中的 OpenKind ，而不是 Nat ，因此拒绝编译。这可以通过某种类型的转换来弥补：

  data NatToOpen :: Nat  - > * 
  

然后用<$替换 n c $ c> NatToOpen n 在 natToInt -s。

问题1 ：有什么方法可以在不使用类型级别的包装器的情况下，在任何函数中指定 * 之外的其他类型？

2：在我看来，非类的函数可以很好地处理任何类型的类型，例如：

  foo :: （a :: *） - > （a :: *）
 foo = id 
 
 bar = foo（SO）
  

但是在类内部，编译器会抱怨类型不匹配，就像我上面所描述的那样。这是为什么？看起来，非类的函数在类型上是正确的多态，因为上面我实际上指定了 * ，它仍然适用于 Nat -s，好像这些种类被简单地忽略了一样。

解决方案

值总是有类型的类型 * 涉及拆箱的异常？），所以没有什么可以应用函数或将其作为一种参数来使用。

在最后一个例子中，将 foo 应用于 Nat 的未提升版本：值为 S 和 O ，它们的类型是 Nat ，它具有 * 。在类定义中，您使用签名来提供 Nat 作为一种签名，这意味着提升版本，其中 S 和 O 是类型。

NatToOpen type只是以通常的方式使用幻像类型，但幻像类型参数为非 * 类。

这个区别对于 DataKinds 也不是新的。例如，没有值的类型是 Maybe :: * - > * ，与类型不同。也许a :: * ，它是 Nothing 类型。

Take the following code:

{-# LANGUAGE KindSignatures, DataKinds #-}

data Nat = O | S Nat

class NatToInt (n :: Nat) where
    natToInt :: n -> Int

instance NatToInt O where
    natToInt _ = 0

instance (NatToInt n) => NatToInt (S n) where
    natToInt _ = 1 + natToInt (undefined :: n)

GHC informs us that it expects an OpenKind in the type specification of natToInt instead of a Nat and thus refuses to compile. This can be remedied by some kind casting:

data NatToOpen :: Nat -> *

and then replacing n with NatToOpen n in t the natToInt-s.

Question 1: is there some way to specify kinds other than * in any function without using type-level wrappers?

Question 2: It appears to me that non-class functions will happily work with types of any kind, for example:

foo :: (a :: *) -> (a :: *)
foo = id

bar = foo (S O)

but inside classes the compiler will complain about kind mismatches, as I described above. Why is that? It doesn't seem that non-class functions are properly polymorphic in kinds, because above I actually specified *, and it still works with Nat-s, as if the kinds were simply ignored.

解决方案

Values always have types of kind * (possibly with some weird exceptions involving unboxing?), so there's nothing you can apply a function to or take as an argument that would have some other kind.

In your final example, you're applying foo to the unlifted version of Nat: the values are S and O, and their type is Nat, which has kind *. In the class definition, you give Nat as a kind using a signature, which means the lifted version, where S and O are types.

The NatToOpen type is just using phantom types in the usual way, but with a phantom type parameter of a non-* kind.

This distinction is not new with DataKinds, either. For example, there are no values whose type is Maybe :: * -> *, as distinct from the type forall a. Maybe a :: *, which is the type of Nothing.

这篇关于功能类型的种类的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！