haskell - 如何避免必须明确编写复合KnownNat约束？

我有一个类型类，它施加一个KnownNat约束：

class KnownNat (Card a) => HasFin a where
  type Card a :: Nat
  ...

而且，我有几个基本的“构建块”类型的此类实例：

instance HasFin () where
  type Card () = 1
  ...

instance HasFin Bool where
  type Card Bool = 2
  ...

我计划使用总和和乘积从这些构件类型中构建许多“复合”类型。当前，当我为以下一种复合类型的实例KnownNat时，我必须显式地编写复合HasFin约束：

instance (HasFin a, HasFin b, KnownNat (Card a + Card b)) => HasFin (Either a b) where
  type Card (Either a b) = Card a + Card b
  ...

我真的不想不必在上面的代码中写：KnownNat (Card a + Card b)。

是否有任何类型检查器插件，能够自动从(HasFin a, HasFin b) =>推断到(KnownNat (Card a + Card b)) =>？

如果失败，我是否可以写一个包含相同推断的蕴含物？

最佳答案

是的，有这样的插件！ ghc-typelits-knownnat

用法示例：

-- Install ghc-typelits-knownnat via your favorite build tool like any other package
-- then only this line needs to be added to enable the plugin
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}

-- Nothing special to be done otherwise, type-level programming as usual.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Card where

import GHC.TypeLits

class KnownNat (Card a) => HasFin a where
  type Card a :: Nat

instance HasFin () where
  type Card () = 1

instance (HasFin a, HasFin b) => HasFin (Either a b) where
  type Card (Either a b) = Card a + Card b

这是使用constraints库的没有插件的另一种技术。它定义了GADT以将约束和包含条件捕获为价值级别的字典，并提供了一些公理，包括​​(KnownNat a, KnownNat b) :- KnownNat (a + b)包含条件。

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}

module Card where

import Data.Constraint
import Data.Constraint.Nat
import GHC.TypeLits

class HasFin a where
  type Card a :: Nat
  card :: Dict (KnownNat (Card a))

instance HasFin () where
  type Card () = 1
  card = Dict

instance (HasFin a, HasFin b) => HasFin (Either a b) where
  type Card (Either a b) = Card a + Card b
  card =
    case (card @a, card @b, plusNat @(Card a) @(Card b)) of
      (Dict, Dict, Sub Dict) -> Dict