如何在Haskell中为存在类型编写getter

Question

感谢这个问题的答案,我已经定义了这样一个类型:

data Chain = forall a. Integral a => Chain [[a]] [a] a a

我需要为每个字段或参数编写一个getter函数,如果你愿意的话.这是我的第一次尝试:

getSimplices (Chain simplices _ _ _) = simplices

但是当我尝试编译ghc时会出现以下错误:

Chain.hs:10:40: error:
• Couldn't match expected type ‘t’ with actual type ‘[[a]]’
    because type variable ‘a’ would escape its scope
  This (rigid, skolem) type variable is bound by
    a pattern with constructor:
      Chain :: forall a. Integral a => [[a]] -> [a] -> a -> a -> Chain,
    in an equation for ‘getSimplices’
    at Chain.hs:10:15-35
• In the expression: simplices
  In an equation for ‘getSimplices’:
      getSimplices (Chain simplices _ _ _) = simplices
• Relevant bindings include
    simplices :: [[a]] (bound at Chain.hs:10:21)
    getSimplices :: Chain -> t (bound at Chain.hs:10:1)

我这样修好了:

getSimplices (Chain simplices _ _ _) = map (map fromIntegral) simplices

即使某种ghc魔法可以防止这种情况对于吸气剂来说非常缓慢,我认为以这种方式修复它只是非常残忍.有没有更好的方法来为这样的类型定义getter？

Answer 1

存在类型的构造函数必然"忘记" a:

Chain :: Integral a => [[a]] -> [[a]] -> a -> a -> Chain

请注意结果类型如何不再依赖于a.

这样做的结果是,当我们模式匹配时Chain,我们不能对什么做出任何假设a.毕竟我们在建造时可以选择任何东西.我们唯一的知识a是它必须是一个整体类型.因此,我们只能使用Integral类型类的方法进行访问.

一般规则是,当我们模式匹配时Chain,我们必须返回一个不依赖的类型的值a.像吸气鬼一样

getter (Chain _ _ x _) = x

违反了这条规则.毕竟,它会有什么类型？

getter :: Chain -> ???

当然不是

getter :: Chain -> a

这意味着我们可以提取任何我们想要的类型Chain.这实际上是行不通的:我们无法自由选择要放入的类型,然后也可以自由选择要取出的类型.

然而,我们可以做的是利用Integral:

getter :: Chain -> Integer
getter (Chain _ _ x _) = fromIntegral x

Integer不依赖a,所以没关系.

Answer 2

你认为getSimplices应该有什么类型？"显而易见"的选择是

getSimplices :: Integral a => Chain -> [[a]]

但这不适用于您的实现,因为调用者getSimplices可以选择a,并且无法保证存储在Chain调用者所需的类型与调用者想要的类型相同,因为您抛弃了该信息.考虑:

let c = Chain [[1 :: Int]] [2] 3 4
in (getSimplices c) :: [[Integer]]

你的两个类型签名明确允许这样做,它们可以适用于任何Integral类型,但是如果没有一些转换,显然也无法工作:Ints必须以Integer某种方式转换为s.

正如评论所说,这是不寻常的.将类型参数添加到Chain会更加简单,以便它跟踪您用于创建它的类型,并将其输出约束为该类型:

data Chain a = Chain [[a]] [a] a a

getSimplices :: Chain a -> [[a]]
getSimplices (Chain xs _ _ _) = xs