英文:
How to type function which takes arguments of a DataKind indexed type instantiated with different indices?
问题
I want to have a data type which contains booleans and doubles strictly in an alternating fashion. Like this:
tw0 = TWInit True
tw1 = TWInit True :-- 0.5
tw2 = TWInit True :-- 0.5 :- False
tw3 = TWInit True :-- 0.5 :- False :-- 0.5
With the following code, all of the above can be typed:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
data TWEnd = TWESample | TWETime
data TimedWord (end :: TWEnd) where
TWInit :: Bool -> TimedWord 'TWESample
TWTime :: TimedWord 'TWESample -> Double -> TimedWord 'TWETime
TWSample :: TimedWord 'TWETime -> Bool -> TimedWord 'TWESample
pattern (:--) :: TimedWord 'TWESample -> Double -> TimedWord 'TWETime
pattern t :-- x = TWTime t x
pattern (:-) :: TimedWord 'TWETime -> Bool -> TimedWord 'TWESample
pattern t :- s = TWSample t s
However, it is not clear to me how to type something like this:
printTimedWord (TWInit sample) = "TWInit " ++ show sample
printTimedWord (tw :-- x) = printTimedWord tw ++ " :-- " ++ show x
printTimedWord (tw :- sample) = printTimedWord tw ++ " :- " ++ show sample
Haskell does not seem to like the above definition because the first argument is both of type TimedWord TWETime
and TimedWord TWESample
. How can I fix this?
英文:
I want to have a data type which contains booleans and doubles strictly in an alternating fashion. Like this:
tw0 = TWInit True
tw1 = TWInit True :-- 0.5
tw2 = TWInit True :-- 0.5 :- False
tw3 = TWInit True :-- 0.5 :- False :-- 0.5
With the following code, all of the above can be typed:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
data TWEnd = TWESample | TWETime
data TimedWord (end :: TWEnd) where
TWInit :: Bool -> TimedWord 'TWESample
TWTime :: TimedWord 'TWESample -> Double -> TimedWord 'TWETime
TWSample :: TimedWord 'TWETime -> Bool -> TimedWord 'TWESample
pattern (:--) :: TimedWord 'TWESample -> Double -> TimedWord 'TWETime
pattern t :-- x = TWTime t x
pattern (:-) :: TimedWord 'TWETime -> Bool -> TimedWord 'TWESample
pattern t :- s = TWSample t s
However, it is not clear to me how to type something like this:
printTimedWord (TWInit sample) = "TWInit " ++ show sample
printTimedWord (tw :-- x) = printTimedWord tw ++ " :-- " ++ show x
printTimedWord (tw :- sample) = printTimedWord tw ++ " :- " ++ show sample
Haskell does not seem to like the above definition because the first argument is both of type TimedWord TWETime
and TimedWord TWESample
. How can I fix this?
答案1
得分: 4
以下是您要翻译的代码部分:
如果您有一个 `TimedWord end`(对于一些未知类型变量 `end`),那么对 GADT 构造进行模式匹配就可以正常工作(尽管需要明确的类型签名):
```haskell
printTimedWord :: TimedWord end -> String
printTimedWord (TWInit sample) = "TWInit " ++ show sample
printTimedWord (TWTime tw x) = printTimedWord tw ++ " :-- " ++ show x
printTimedWord (TWSample tw sample) = printTimedWord tw ++ " :- " ++ show sample
所以您的问题不是“如何接受具有不同类型索引的 GADTs”,而是似乎 模式同义词 与此 GADT 功能不太兼容。我不确定是否不可能编写像 GADT 构造函数一样工作的模式同义词,或者是否需要额外的操作。
然而,从您的简单示例中看来,您可能更愿意使用中缀操作符而不是命名构造函数?因此,修复问题的另一种方法是放弃模式同义词,而是直接在一开始就使用 :--
和 :-
作为构造函数:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
data TWEnd = TWESample | TWETime
data TimedWord (end :: TWEnd) where
TWInit :: Bool -> TimedWord 'TWESample
(:--) :: TimedWord 'TWESample -> Double -> TimedWord 'TWETime
(:-) :: TimedWord 'TWETime -> Bool -> TimedWord 'TWESample
printTimedWord :: TimedWord end -> String
printTimedWord (TWInit sample) = "TWInit " ++ show sample
printTimedWord (tw :-- x) = printTimedWord tw ++ " :-- " ++ show x
printTimedWord (tw :- sample) = printTimedWord tw ++ " :- " ++ show sample
我知道这可能不是您整个问题的解决方案,但如果您将运算符用作实际构造函数并为它们提供中缀声明,那么 GHC 可以为您简单地派生一个 Show
实例,基本上与您尝试使用 printTimedWord
做的事情相匹配(但如果您不使用 GHC2021
,则需要 StandaloneDeriving
):
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE StandaloneDeriving #-}
data TWEnd = TWESample | TWETime
data TimedWord (end :: TWEnd) where
TWInit :: Bool -> TimedWord 'TWESample
(:--) :: TimedWord 'TWESample -> Double -> TimedWord 'TWETime
(:-) :: TimedWord 'TWETime -> Bool -> TimedWord 'TWESample
printTimedWord :: TimedWord end -> String
printTimedWord (TWInit sample) = "TWInit " ++ show sample
printTimedWord (tw :-- x) = printTimedWord tw ++ " :-- " ++ show x
printTimedWord (tw :- sample) = printTimedWord tw ++ " :- " ++ show sample
infixr 8 :-
infixr 8 :--
deriving instance Show (TimedWord end)
使用这个方法,我们可以看到:
λ printTimedWord $ (TWInit True) :-- 3
"TWInit True :-- 3.0"
λ show $ (TWInit True) :-- 3
"TWInit True :-- 3.0"
因此,您不一定需要实现 printTimedWord
。
(我不知道实际上什么是适当的关联性或优先级,我只是随机选择了一些内容;不管是模式同义词还是实际构造函数,中缀声明可能都是一个好主意。)
英文:
If you have a TimedWord end
(for some unknown type variable end
), then pattern matching on the GADT constructors just works (an explicit type signature is necessary though):
printTimedWord :: TimedWord end -> String
printTimedWord (TWInit sample) = "TWInit " ++ show sample
printTimedWord (TWTime tw x) = printTimedWord tw ++ " :-- " ++ show x
printTimedWord (TWSample tw sample) = printTimedWord tw ++ " :- " ++ show sample
So your problem is not "how to accept GADTs with different type indexes", but rather that it seems pattern synonyms don't play nicely with this GADT feature. I'm not sure if it's impossible to write pattern synonyms that work like GADT constructors, or whether there's just something extra you have to do.
However it seems (at least from your simple example) that you simply would rather use infix operators than named constructors? So an alternative way to fix your problem is to ditch the pattern synonyms and simply use :--
and :-
as the constructors in the first place:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
data TWEnd = TWESample | TWETime
data TimedWord (end :: TWEnd) where
TWInit :: Bool -> TimedWord 'TWESample
(:--) :: TimedWord 'TWESample -> Double -> TimedWord 'TWETime
(:-) :: TimedWord 'TWETime -> Bool -> TimedWord 'TWESample
printTimedWord :: TimedWord end -> String
printTimedWord (TWInit sample) = "TWInit " ++ show sample
printTimedWord (tw :-- x) = printTimedWord tw ++ " :-- " ++ show x
printTimedWord (tw :- sample) = printTimedWord tw ++ " :- " ++ show sample
I know this is unlikely to be your entire problem, but if you use the operators as the real constructors and provide infix declarations for them, then GHC can simply derive a Show
instance for you that basically matches what you're trying to do with printTimedWord
(but requires StandaloneDeriving
, if you're not using GHC2021
):
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE StandaloneDeriving #-}
data TWEnd = TWESample | TWETime
data TimedWord (end :: TWEnd) where
TWInit :: Bool -> TimedWord 'TWESample
(:--) :: TimedWord 'TWESample -> Double -> TimedWord 'TWETime
(:-) :: TimedWord 'TWETime -> Bool -> TimedWord 'TWESample
printTimedWord :: TimedWord end -> String
printTimedWord (TWInit sample) = "TWInit " ++ show sample
printTimedWord (tw :-- x) = printTimedWord tw ++ " :-- " ++ show x
printTimedWord (tw :- sample) = printTimedWord tw ++ " :- " ++ show sample
infixr 8 :-
infixr 8 :--
deriving instance Show (TimedWord end)
With this we can see:
λ printTimedWord $ (TWInit True) :-- 3
"TWInit True :-- 3.0"
λ show $ (TWInit True) :-- 3
"TWInit True :-- 3.0"
So you don't necessarily need to implement printTimedWord
at all.
(I have no idea what associativity or precedence is actually appropriate, I just picked something arbitrarily; with no infix declarations the derived Show
instance prints the constructors in prefix form like (:--) (TWInit True) 3.0
. Infix declarations are probably a good idea regardless though, whether they're pattern synonyms or real constructors)
答案2
得分: 4
我不太看得出为什么在这里要使用模式同义词;如果有疑问,我会始终使用GADT构造函数,如本的答案中所示。
也就是说,这里是如何使用模式同义词的:
pattern (:%) :: () => (end ~ 'TWETime)
=> TimedWord 'TWESample -> Double -> TimedWord end
pattern t :% x = TWTime t x
pattern (:-) :: () => (end ~ 'TWESample)
=> TimedWord 'TWETime -> Bool -> TimedWord end
pattern t :- s = TWSample t s
printTimedWord :: TimedWord end -> String
printTimedWord (TWInit sample) = "TWInit " ++ show sample
printTimedWord (tw :% x) = printTimedWord tw ++ " :% " ++ show x
printTimedWord (tw :- sample) = printTimedWord tw ++ " :- " ++ show sample
关键是将 end ~ 'TWESample
的约束放在模式同义词签名的“提供”位置,而不是“必需”位置。参见pattern synonyms / static semantics。
英文:
I don't really see any reason why you'd use pattern synonyms here; in doubt I'd always just use the GADT constructor as in Ben's answer.
That said, here's how to do it with pattern synonyms:
pattern (:%) :: () => (end ~ 'TWETime)
=> TimedWord 'TWESample -> Double -> TimedWord end
pattern t :% x = TWTime t x
pattern (:-) :: () => (end ~ 'TWESample)
=> TimedWord 'TWETime -> Bool -> TimedWord end
pattern t :- s = TWSample t s
printTimedWord :: TimedWord end -> String
printTimedWord (TWInit sample) = "TWInit " ++ show sample
printTimedWord (tw :% x) = printTimedWord tw ++ " :% " ++ show x
printTimedWord (tw :- sample) = printTimedWord tw ++ " :- " ++ show sample
The trick is to have the end ~ 'TWESample
constraint not in the "required" position, but in the "provided" position of the synonyms' signature. Cf. pattern synonyms / static semantics.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库,让每个人都能够通过互相帮助和分享经验来进步。
评论