不寻常的种类和数据构造器 [英] Unusual Kinds and Data Constructors

问题描述

我不知道我没有注意到这一点，但数据构造函数和函数定义都不能使用 * 以外的类型，它的变体 * - > * 等等，由于（ - >）的亲笔签名，甚至在 -XPolyKinds


以下是我尝试过的代码：



  { - ＃LANGUAGE DataKinds＃ - } 
 { - ＃LANGUAGE KindSignatures＃ - } 
 
数据Nat = S Nat | Z 
 
 data Foo where 
 Foo ::'Z  - > Foo  - 失败
 
 foo ::'Z  - > Int  -  Fails 
 foo _ = 1 
  

我得到的错误如下：



 < interactive>：8：12：
预期类型，但'Z' '
在'foo'的签名中：foo ::'Z  - > Int 
  

为什么我们不应该允许与非传统类型的模式匹配？

解决方案

没有 1 这样的事情，类型不是 * 。 Kind * 是类型的类型，很像 Int 是 键入机器大小的数字;其他类型可能包含类似于类型的东西，或者可以转换为类型或用于索引类型或其他类型的东西。但不是类型，而仅仅是类型级别实体。

---

¹ _{通常情况下，我忽略unbox-kinds。}

I don't know how I didn't notice this, but data constructors and function definitions alike can't use types with kinds other than * and it's variants * -> * etc., due to (->)'s kind signature, even under -XPolyKinds.

Here is the code I have tried:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

data Nat = S Nat | Z

data Foo where
  Foo :: 'Z -> Foo -- Fails

foo :: 'Z -> Int -- Fails
foo _ = 1

The error I'm getting is the following:

<interactive>:8:12:
    Expected a type, but ‘Z’ has kind ‘Nat’
    In the type signature for ‘foo’: foo :: 'Z -> Int

Why shouldn't we allow pattern matching with non-traditional kinds?

解决方案

There is no¹ such thing as "types with kinds other than *". Kind * is the kind for types, much like Int is the type for machine-sized numbers; other kinds may contain stuff that resembles types or can be converted to types or is used to index types or whatever – but is not types as such, merely "type level entities".

---

¹_{As usually, I disregard unbox-kinds here.}

这篇关于不寻常的种类和数据构造器的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！