相关疑难解决方法(0)

因此,在我不断尝试通过小型Haskell练习半理解Curry-Howard时,我已经陷入了困境:

{-# LANGUAGE GADTs #-}

import Data.Void

type Not a = a -> Void

-- | The type of type equality proofs, which can only be instantiated if a = b.
data Equal a b where
    Refl :: Equal a a

-- | Derive a contradiction from a putative proof of @Equal Int Char@.
intIsNotChar :: Not (Equal Int Char)
intIsNotChar intIsChar = ???

很明显,这种类型Equal Int Char没有(非底层)居民,因此在语义上应该有一个absurdEquality :: Equal Int Char -> a功能......但对于我的生活,我无法想出任何方式来编写除了使用之外的其他方法undefined.

所以要么: …

是否有可能做类似的事情

class T a
class U a
instance U ()
instance ( NOT U a ) => T a

上下文:我正在尝试编写一个函数,它接受HLists并删除某种类型的元素(这里是单元类型).

我觉得开放世界的假设可能存在一些问题,但即使能够以硬编码方式(而不是NOT U a,类似NOT~())这样做也应该是可能的.

编辑:正如CA McMann的评论所指出的,这个问题几乎与我的完全相同.如果主持人想要关闭这个,请随意.

我试图在我正在使用的类型的类型参数上使用一些相当复杂的条件来定义类型类的实例，并且认为一个有用的方法是声明一个封闭的类型系列，该系列在我定义的实例之间进行选择。不幸的是，我根本无法让这个想法发挥作用，因为 GHC 抱怨这些实例是重复的。这是一个简化的示例，它给出了我所看到的相同错误：

{-# LANGUAGE FlexibleInstances, TypeFamilies #-}
data MyContainer a = NoValue | OneValue a | TwoValues a a

data Yes
data No

type family IsInt t where
    IsInt Int = Yes
    IsInt a   = No

instance IsInt t ~ Yes => Show (MyContainer t) where
    show _ = "Type is int"
instance IsInt t ~ No => Show (MyContainer t) where
    show _ = "Type is not int"

我看到的错误是：

src/Test.hs:11:10:
    Duplicate instance declarations:
      instance (IsInt t ~ Yes) …