在没有专门使用构造函数的情况下获取GADT风格声明中的约束？

考虑以下几点：在没有专门使用构造函数的情况下获取GADT风格声明中的约束？

{-# LANGUAGE GADTs, GADTSyntax #-} 

data Test a where 
    Test :: Ord a => { first :: a, second :: a } -> Test a 

comp :: Test a -> Bool 
comp (Test fst snd) = fst < snd

构造Test与一个Ord约束声明。在comp，我已经明确采取Test构建的参数，这给Ord约束允许我使用<

现在，假设我想写：

comp' :: Test a -> Bool 
comp' x = (first x) < (second x)

使用投影功能，以获得第一和第二元素。这是而不是没问题，因为我的参数x不是（必然）用Test构建的，所以没有Ord约束。

所以，我的问题，是有办法把参数作为刚刚x但仍不知为什么从Test构造的Ord约束，而不必“解压”或在Test构造模式匹配或添加约束我的功能？

至于为什么我想这一点，我有一个构造数据类型采取了许多价值观，其中之一，我只需要在这个特殊的功能，所以拆包它使我的功能不必要的冗长：

myFunction :: Thing -> ... 
myFunction (Thing _ _ _ _ need _ _) ...

与之相对

myFunction t = ... (need t)

来源

2016-07-29 cemulate

您可以使用'myFunction t @ Thing {} = ...'。 – Alec

'myfunction Thing {need = x}'这提供了'Ord'字典，而且'need'字段的值也已经解压到'x'中。还有一个扩展可以让你编写'myFunction Thing {need}'，并且在主体中你可以使用'need'这个名字来引用参数'need'字段的值。 – Bakuriu

谢谢你们，不知道那种语法！ – cemulate

您可以定义它提取所有的约束从构造函数：

data Test a where 
    Test :: Ord a => { first :: a, second :: a } -> Test a 

openTest :: Test a -> (Ord a => r) -> r 
openTest Test{} x = x

然后，您可以编写

comp :: Test a -> Bool 
comp x = openTest x $ first x < second x

但要注意的openTest的实施完全是微不足道的 - 这是打字少，只是内联模式匹配：

comp' :: Test a -> Bool 
comp' [email protected]{} = first x < second x

还要注意这一点（即Test{}语法）将与任何构造函数一起工作，即使它不是一个记录构造函数。您的实际功能，可以简单地表述为

myFunction [email protected]{} = ... (need t) ...

或等价

openThing :: Thing a -> (ThingConstraints a => r) -> r 
openThing Thing{} x = x 

myFunction t = ... (openThing $ need t) ...

最后，您还可以定义一个函数来提取特定领域，以及适用于该领域的约束，这对于有很多约束条件的大型建设者非常有用：

first' :: Test a -> (Ord a => a -> r) -> r 
first' [email protected]{} x = x (first t)

来源

2016-07-29 15:04:24 user2407038

在没有专门使用构造函数的情况下获取GADT风格声明中的约束？

回答

相关问题