在Haskell中只允许不同的“任何”类型

html5 • • 问答

假设我们有一个带签名的函数

foo :: a -> b -> Int

是否可以强制执行约束以确保a和b不同？那是

foo :: Int -> String -> Int -- ok
foo :: Int -> Int    -> Int -- not ok

这个问题的目的是了解有关 Haskell 的更多信息，并可能解决我面临的设计问题。如果 a == b，我的特殊情况没有意义，所以我想在编译器级别禁止它。我可能可以通过完全不同的设计让这个问题消失，但这不是现在的重点 - 潘多拉盒子已经打开，我想了解是否可以在类型级别上进行相等约束。

回答

像这样？

{-# LANGUAGE DataKinds #-}
module TyEq where

import Data.Type.Equality (type (==))
import GHC.TypeLits
import Data.Kind (Constraint)

class ((a == b) ~ eq) => Foo a b eq where
  foo :: a -> b -> Int

instance (TypeError ('Text "NAUGHTY!"), (a == b) ~ True) => Foo a b 'True where
  foo _ _ = error "The types have failed us!"

instance (a == b) ~ False => Foo a b 'False where
  foo _ _ = 42

--_ = foo True True -- NAUGHTY!
_ = foo () True
_ = foo True (42 :: Int)

请注意eqFoo 类型类中如何需要索引，或者尽管实例上下文不同（仅考虑头部），但我们仍会收到“重复实例”错误。

我们可以使用特定用途的类型系列来简化一下：

type family Check a b :: Constraint where
  Check a a = TypeError ('Text "VERY NAUGHTY!")
  Check a b = ()

foo' :: Check a b => a -> b -> Int
foo' _ _ = 42

--_ = foo' True True -- VERY NAUGHTY!
_ = foo' () True
_ = foo' True (42 :: Int)

我很确定我已经从 Sandy Maguire 的“Thinking with Types”中学到了这一切，我真诚地向所有感兴趣的人推荐：)

回答

该类型a :~: b -> Void在a和完全不同时（由一个总函数）居住b，因此一种轻量级的方法是将其作为参数。然后，您可以要求编译器检查调用者是否提供了带有-Wincomplete-patterns. 一个完整的示例可能如下所示：

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}

import Data.Void
import Data.Type.Equality

foo :: (a :~: b -> Void) -> a -> b -> Int
foo _ _ _ = 0

fooUseGood :: Int
fooUseGood = foo (case) True () -- accepted, no warning

fooUseBad :: Int
fooUseBad = foo (case) () () -- warning: Patterns not matched: Refl

以上是在Haskell中只允许不同的“任何”类型的全部内容。
THE END
分享
二维码
< <上一篇
下一篇>>