时间戳

首页 > 解决方案 > 在 Haskell 中只允许不同的“任何”类型

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

问题描述

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

foo :: a -> b -> Int

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

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

这个问题的目的是了解更多关于 Haskell 的信息，也许可以解决我面临的设计问题。如果 a == b，我的特殊情况没有意义，所以我想在编译器级别禁止这种情况。我可能可以用不同的设计完全解决这个问题，但现在不是重点——潘多拉魔盒已经打开，我想知道类型级别的等式约束是否可能。

标签： haskell

解决方案

像这样？

{-# 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)

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

我们可以使用特定目的类型族来简化这一点：

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”中学到了这一切，我真诚地向所有感兴趣的人推荐 :)

推荐阅读