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

Question

我正在学习哈斯克尔.我试过的时候:

Prelude> data Binary = 0 | 1

我有:

<interactive>:2:15:
    Illegal literal in type (use -XDataKinds to enable): 0

即使我开始使用ghci ghci -XDataKinds

我还有:

<interactive>:2:15:
    parse error in constructor in data/newtype declaration: 0

任何人都可以对此有所了解吗？

Answer 1

基本上,不允许使用0和1之类的数字作为用户定义类型的数据构造函数的名称.从语法上讲,它们必须是以大写字母开头的单词.例如,您可以这样做:

data Binary = O | I

(注意那些是大写字母'o'和'i',而不是数字零和一.)

Answer 2

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仍需要在括号内.我认为逻辑上这个特殊形式应该没有括号,但事实并非如此.

考虑到这一点,我认为通过建议有一些方法可以使扩展适合0该位置,Haskell会造成不必要的混乱.然而,分析的方式和类型/类型的检查是在GHC不同的阶段,它可能是太复杂,赶上这在一个更加用户友好的方式,它甚至可能最终意味着以后的事有效.