haskell - 如何在类型族中为使用类型相等的约束定义自定义类型错误？

Question

因此，可以像这样定义成员约束：

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}

module Whatever where

type family MemberB (x :: k) (l :: [k]) where
  MemberB _ '[]      = 'False
  MemberB a (a : xs) = 'True
  MemberB a (b : xs) = MemberB a xs

type Member x xs = MemberB x xs ~ 'True

data Configuration = A | B | C

data Action (configuration :: Configuration) where
  Action1 :: Member cfg '[ 'A ]     => Action cfg
  Action2 :: Member cfg '[ 'B, 'C ] => Action cfg
  Action3 :: Member cfg '[ 'A, 'C ] => Action cfg

exhaustive :: Action 'A -> ()
exhaustive Action1 = ()
exhaustive Action3 = ()
exhaustive Action2 = ()

但是我们得到的错误信息不是很丰富：

 • Couldn't match type ‘'False’ with ‘'True’
   Inaccessible code in
     a pattern with constructor:
       Action2 :: forall (cfg :: Configuration).
                  Member cfg '['B, 'C] =>
                  Action cfg,
     in an equation for ‘exhaustive’
 • In the pattern: Action2
   In an equation for ‘exhaustive’: exhaustive Action2 = () (intero)

使用新功能来改进此消息会很好TypeError，但是，一个天真的解决方案会吞噬错误：

import GHC.TypeLits

type family MemberB (x :: k) (l :: [k]) where
  MemberB _ '[]      = TypeError ('Text "not a member")
  MemberB a (a : xs) = 'True
  MemberB a (b : xs) = MemberB a xs

似乎，也许，TypeError表现为任何类型，因此它与'True?

有没有办法得到一个很好的类型错误，同时保留成员行为？

标签： haskelltype-constraintstype-families

Answer 1

好吧，它不使用TypeError，但无论如何你可能会觉得它很有趣：

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}

module Whatever where

data IsMember k = IsMember | Isn'tMember k [k]

type family MemberB (x :: k) (l :: [k]) (orig :: [k]) where
  MemberB a '[]      ys = 'Isn'tMember a ys
  MemberB a (a : xs) ys = 'IsMember
  MemberB a (b : xs) ys = MemberB a xs ys

type Member x xs = MemberB x xs xs ~ 'IsMember

data Configuration = A | B | C

data Action (configuration :: Configuration) where
  Action1 :: Member cfg '[ 'A ]     => Action cfg
  Action2 :: Member cfg '[ 'B, 'C ] => Action cfg
  Action3 :: Member cfg '[ 'A, 'C ] => Action cfg

exhaustive :: Action 'A -> ()
exhaustive Action1 = ()
exhaustive Action3 = ()
exhaustive Action2 = ()

该错误现在提供了更多信息：

test.hs:32:16: error:
    • Couldn't match type ‘'Isn'tMember 'A '['B, 'C]’ with ‘'IsMember’
      Inaccessible code in
        a pattern with constructor:
          Action2 :: forall (cfg :: Configuration).
                     Member cfg '['B, 'C] =>
                     Action cfg,
        in an equation for ‘exhaustive’
    • In the pattern: Action2
      In an equation for ‘exhaustive’: exhaustive Action2 = ()
   |
32 |     exhaustive Action2 = ()
   |                ^^^^^^^