1. 首页
  2. 问答
  3. haskell数据定义错误 - 类型中的非法文字（使用-XDataKinds启用）

haskell数据定义错误 - 类型中的非法文字（使用-XDataKinds启用）

2014-09-25 49 views

回答

6

data Binary = 0 | 1是不正常的定义数据类型的形式。 data定义需要数据构造函数和0和1对于它们来说不是合法语法，因为它们已经用于数字文字。这是第二条错误消息试图告诉你的，并且是基本的Haskell。对于数据构造最常见的语法是一个大写的话，那么你可能想要的东西更像

data Binary = Zero | One

注意：此消息的其余部分是先进的东西，你可能不需要，但我觉得解释关于你为什么得到第一个关于-XDataKinds的错误消息。

随着DataKinds延伸，0和1做了别样的成为合法的“类型”（被称为Nat，而事实上“厚道”是这里的技术术语），用于高级型级别的编程，并与还有几个扩展它是可能获得包含它们的数据定义。

请注意，下面的例子可能不是真的有用，我只是拼凑在一起，以显示它是可能的。在实践中，除非你在做相当先进的东西，data Binary = Zero | One可能更像你想要的。

{-# LANGUAGE DataKinds, KindSignatures #-} 

import GHC.TypeLits (Nat) 

data Proxy (n :: Nat) = Proxy 
data WeirdBinary = Zero (Proxy 0) | One (Proxy 1)

我还没有真正能够使工作（虽然我只尝试了一会儿）是什么，开始data Binary = 0。我得到的最接近像

class (n :: Nat) /// a where 

data Binary = (0 /// Bool) => ThisIsSilly

奇怪的东西，其中0仍需要在括号内。我想逻辑上这种特殊的形式应该没有括号的工作，但它不。

鉴于此，我认为Haskell正在被不必要地混淆，因为暗示有一些方法可以使扩展符合0。然而，使用分析和类型/类型检查的方式在GHC中是分开的阶段，以更加用户友好的方式来捕捉它可能过于复杂，甚至最终可能意味着未来有效。

来源

2014-09-25 03:41:15

10

基本上，您不允许使用数字0和1作为用户定义类型的数据构造函数的名称。在句法上，它们必须是以大写字母开头的单词。例如，你可以这样做，而不是：

data Binary = O | I

（请注意，这些都是大写字母“O”和“我”，而不是数字零和一。）

来源

2014-09-25 03:26:00 kini

3

第一个错误是说，像0和1（或实际上"foo"，[1, 2, 3]，'Z'）文字值是无效的类型声明在所有。

您无法声明包含现有类型元素的新类型，因为它看起来像您正在尝试使用data Binday = 0 | 1。类型只能包含所有另一种类型的成员（这就是为什么你包括其他类型的在类型表达式，不值）。

DataKinds扩展引入了新的表单类型（我不会在这里介绍），这意味着文字值可以出现在某些位置的类型声明中。所以它确实解决了“非法文字类型”错误，但即使与DataKinds文字值仍不允许在那位置。

第二个错误是告诉你编译器无法解析“0”作为构造函数名称。施工人员必须以大写字母开头，其中0显然没有。

我之前撒谎时说过“类型只能包含所有的其他类型的成员”。实际上，新类型不能包含任何现有类型的成员;它们包含不属于任何现有类型的全新值。这是通过要求所有新类型的值由构造函数来标记的;在data声明中声明了可能的构造函数，并且这是在写入0和1的地方必须找到构造函数的地方。

0已经是现有的类型Int 的一员，所以它永远是你的新类型Binary的成员，无论你如何申报。

你可以得到一个0这是包含在Binary类型的值：ConstructorName 0，也许。但是，您将不得不声明Binary类型为data Binary = ConstructorName Int | ...;在类型声明中的构造函数名称后面应该有类型，用于标识可以放置在新的Binary值的“插槽”中的值的类型。还有也没有办法使该“槽”只能包含0或1，它必须是一个整个类型。

或为中缀运营商构造一个冒号，但在这里，这是不相关的。

实际上文字表达0过载，因此它可能是代表任何数字类型的零元素，但我说的是一个是Int之一。

来源

2014-09-25 04:47:37 Ben

相关问题

 相关问题