具有约束的Haskell类型同义词声明可能吗？

Question

假设我想为Int的所有列表创建一个类型同义词.

我可以:

type NumberList = [Int]

但是如果我想调用包含数字NumberList的所有列表呢？我如何设置约束并说所有[a]只要"Num a"应该被称为相同？

编辑::看到答案后,我重新思考.看起来我反对Haskell背后的一个基本思想,奖励相对较小(只是一个正式的问题).我决定这样做:如果一个类型需要两个相同的实例,只有Int或Float不同,那么它们之间的差异太小,无法保证完成Int和Float的使用所需的解决方法但是调用它们是同一个东西,这就是为什么我必须将使用限制在其中之一.但是,如果有一个重要的原因,为什么我应该同时拥有两者,那么我可以在实例的名称中反映这个重要的原因,从而通过这样做避免问题:

data Thing = Thing_A(String, String Float) | Thing_B(String,String,Int)

---从而坚持Haskell的打字系统,仍然接受它们作为数据类型Thing.我最初想做的是

data Thing = Thing(String, String, Float) | Thing(String, String, Int)

Answer 1

这对应于存在量化.在伪Haskell中,

type NumberList = exists a . Num a => [a]

我说«伪»因为GHC不允许动态引入存在量词 - 你需要为它创建一个单独的数据类型.

现在,大多数类型你使用箭头左侧的NumberList,其中«exists»有效地将其含义改为«forall».

也就是说,而不是写作

isIncreasing :: NumberList -> Bool

这是一样的

isIncreasing :: (exists a . Num a => [a]) -> Bool

你可以写

isIncreasing :: forall a . Num a => [a] -> Bool

或者干脆

isIncreasing :: Num a => [a] -> Bool

当然,拥有类型同义词似乎代码较少,但它也有缺点.顺便说一下,这些缺点是面向对象编程的典型特征,它基于存在方法.

例如,您想要连接两个列表.通常你会写

(++) :: forall a . [a] -> [a] -> [a]

(forall为了清楚起见,再次没有必要并添加).由于a整个签名是相同的,因此可确保您连接相同类型的列表.

我们如何连接两个数字列表？一个签名

(++) :: NumberList -> NumberList -> NumberList

不起作用,因为一个列表可能包含Ints而另一个列表可能包含双打.结果NumberList必须包含单个类型的值.

或者,比方说,您想要找到列表元素的总和.

通常你写

sum :: Num a => [a] -> a

请注意,结果类型与列表元素的类型相同.唉,我们不能为NumberList做同样的事情!

sum :: NumberList -> ???

结果类型是什么？我们也可以在那里应用存在量化.

sum :: NumberList -> (exists a . Num a => a)

但是现在原始列表类型和总和类型之间的连接丢失了 - 至少对于Haskell的类型系统而言.如果你决定写一个像这样的函数

multiplySum :: Integer -> [Integer] -> Integer
multiplySum x ys = x * sum ys

然后你会得到一个类型错误,因为它sum ys可能是任何类型,不一定是Integer类型.

如果你将所有东西都推向极端并使每种类型都存在量化 - 那么它就会起作用 - 但是你最终会用另一种面向对象的语言来解决所有问题.

(也就是说,当然存在一些用于存在量化的好用例.)

Answer 2

使用数据和参数,而不是存在来获取上下文

我想如果你想要的话

data Thing = Good [(Char,Int)] | Bad String | Indifferent Leg

但有时也是

data Thing = Good [(Char,Float)] | Bad String | Indifferent Arm

你可以定义

data Thing num bodypart = Good [(Char,num)] | Bad String | Indifferent bodypart

或者如果你想确保num它总是数字,你可以做到

data Num num => Thing num bodypart = Good [(Char,num)] | Bad String | Indifferent bodypart

最后,您可以bodypart通过定义自己的类来限制允许的类型:

class Body a where
   -- some useful function(s) here

instance Body Leg where
   -- define useful function(s) on Legs
instance Body Arm
   -- define useful function(s) on Arms

data (Num num,Body bodypart) => Thing num bodypart = 
                                                             Good [(Char,num)] | Bad String | Indifferent bodypart

我想从通过FORALL构造或通过使用GADTs存在类型劝阻你,因为添加num参数数据类型是相当实际上更有用,即使它需要更多的输入.

类型同义词的约束？

请注意,当您使用约束时

data (Num num) => Thing num = T [(Char,num)]

实际上只是将构造函数的类型更改T为

T :: (Num num) => [(Char,num)] -> Thing num

而不是T :: [(Char,num)] -> Thing num.这意味着每次使用T时都需要有一个上下文(Num num),但这正是你想要的 - 阻止人们将数据放入非数字的数据类型中.

这个事实的结果是你不能写

type Num num => [(Char,num)]

因为没有数据构造函数T需要上下文(Num num); 如果我有[('4',False)],它会自动匹配类型,[(Char,num)]因为它是同义词.在确定实际类型之前,编译器不能在代码中运行查找实例.在这种data情况下,它有一个构造函数T告诉它类型,它可以保证有一个Num num实例,因为它检查了你对函数的使用T.不T,没有背景.