如何编写接受用不同索引实例化的 DataKind 类型参数的函数?

huangapple go评论55阅读模式
英文:

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.

huangapple
  • 本文由 发表于 2023年6月15日 13:41:00
  • 转载请务必保留本文链接:https://go.coder-hub.com/76479418.html
匿名

发表评论

匿名网友

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen:

确定