函数中的各种类型

Question

请使用以下代码:

{-# 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告诉我们它期望OpenKind在类型规范中natToInt而不是a Nat,因此拒绝编译.这可以通过某种铸造来解决:

data NatToOpen :: Nat -> *

然后更换n与NatToOpen n在t时的natToInt-s.

问题1:有没有办法*在不使用类型级包装器的情况下指定除任何函数之外的其他类型？

问题2:在我看来,非类函数将很乐意使用任何类型的类型,例如:

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

bar = foo (S O)

但是在内部类中,编译器会抱怨类型不匹配,如上所述.这是为什么？似乎非类函数在各种类型中都是正确的多态,因为上面我实际指定了 *它,它仍然可以使用Nat-s,就好像这些类被简单地忽略了一样.

Answer 1

值总是有类型的类型*(可能有一些涉及拆箱的奇怪异常？),所以没有什么可以将函数应用于或作为具有其他类型的参数.

在你的最后一个例子中,你正在应用于未foo提升的版本Nat:值是S和O,以及它们的类型是Nat哪种类型*.在类定义,你给Nat作为使用签名的一种,这意味着解禁版本,其中S和O是类型.

该NatToOpen类型只是以通常的方式使用幻像类型,但是使用非*类型的幻像类型参数.

这种区别也不是新的DataKinds.例如,没有类型Maybe :: * -> *的类型forall a. Maybe a :: *,与类型不同,它是类型Nothing.