如何在类型级别上进行EmptyCase

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实现类TAbsurdVoid 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)