如何为使用类型相等性的约束在类型族中定义自定义类型错误? [英] How to define a custom type error within a type family for a constraint that uses type equality?

问题描述

因此，可以像这样定义成员资格约束:

So, one can define a membership constraint like so:

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

但是我们得到的错误消息不是很有用:

But the error message we get is not very informative:

 • 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功能来改进此消息，但是，一个幼稚的解决方案会吞噬该错误:

It'd be nice to use the new TypeError feature to improve on this message, however, a naive solution gobbles the error:

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统一起来很快乐?

It seems that, maybe, TypeError behaves as any type, and so it unifies happily with 'True?

在保留成员资格行为的同时，有没有办法得到一个不错的类型错误?

Is there a way to get a nice type error, while preserving the membership behavior?

推荐答案

好吧，它不使用TypeError，但是无论如何，您可能会发现它很有趣:

Well, it doesn't use TypeError, but you might find it interesting anyway:

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

该错误现在可以提供更多信息:

The error is a bit more informative now:

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 = ()
   |                ^^^^^^^

这篇关于如何为使用类型相等性的约束在类型族中定义自定义类型错误?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！