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

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一个具有关联类型 kind 的类的成员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这可以通过return nota而是 a来解决Proxy (TAbsurdVoid a)：

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