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

Question

我有一个类型类，它强加了 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)) => ?

如果做不到这一点，我可以写一个提供相同推断的蕴涵吗？

Answer 1

是的，有这样的插件! 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