haskell - 如何在类型级别清空大小写

Question

使用 EmptyCase ，可以实现以下功能:

{-# LANGUAGE EmptyCase, EmptyDataDecls #-}

data Void

absurd :: Void -> a
absurd v = case v of

与 DataKinds ，数据类型可以提升到种类级别(它们的构造函数被提升为类型构造函数)。这适用于无人居住的数据类型，如 Void也是。
这里的问题是是否有一种方法可以写成 absurd对于无人居住的种类:

tabsurd :: Proxy (_ :: Void) -> a
tabsurd = _

这实际上是“类型级别的 EmptyCase”的一种形式。在合理范围内，请随意替换 Proxy与其他一些合适的类型(例如 TypeRep )。
注意:我知道我可以求助于 error或类似的不安全技术，但我想看看如果该类型不是无人居住，是否有办法做到这一点。因此，对于我们提出的任何技术，都不应该使用相同的技术来实现以下功能:

data Unit = Unit

notsoabsurd :: Proxy (_ :: Unit) -> a
notsoabsurd = _

Answer 1

模式匹配的类型级别等价物是类型类(好吧，也是类型族，但它们在这里不适用，因为您想要一个术语级别的结果)。
所以你可以想象 tabsurd类的成员，该类的关联类型为 Void :

class TAbsurd a where
  type TAbsurdVoid a :: Void
  tabsurd :: a

在这里，tabsurd将有类型签名 tabsurd :: TAbsurd a => a ，但如果你坚持使用 Proxy ，您显然可以轻松地将一个转换为另一个:

pabsurd :: TAbsurd a => Proxy a -> a
pabsurd _ = tabsurd

所以调用这样的函数或以任何其他方式使用它大概是不可能的，因为你不能实现类 TAbsurd a对于任何 a ，因为您无法提供类型 TAbsurdVoid a .

根据您的要求，同样的方法对 Unit 也适用。 :

data Unit = Unit

class V a where
  type VU a :: Unit
  uabsurd :: a

instance V Int where
  type VU Int = 'Unit
  uabsurd = 42

但是请记住，在 Haskell 中，任何类型(包括 Void )都可能存在于非终止类型族中。例如，这有效:

type family F a :: x

instance TAbsurd Int where
  type TAbsurdVoid Int = F String
  tabsurd = 42

然而，这个限制类似于任何类型(包括 Void )被值 undefined 所占据。在学期级别，以便您实际上可以调用 absurd像这样:

x = absurd undefined

与类型级别的区别在于您实际上可以调用函数tabsurd。 (给定上面的实例)，它将返回 42 :

print (tabsurd :: Int)

这可以通过 tabsurd 来解决。不返回 a , 但是一个 Proxy (TAbsurdVoid a) :

class TAbsurd a where
  type TAbsurdVoid a :: Void
  tabsurd :: Proxy (TAbsurdVoid a)