haskell - 如何将数据类型带入值(value)级别？

Question

我的代码中有这样的东西:

data SomeKind = Kind1 | Kind2 deriving Eq

data SomeValue (t :: SomeKind) = SomeValue

someValue1 :: SomeValue Kind1
someValue1 = SomeValue

someValue2 :: SomeValue Kind2
someValue2 = SomeValue

我想将类型级别的那种类型提升到值级别，可能是这样的:

valueKind :: SomeValue a -> SomeKind

这将:

valueKind someValue1 == Kind1
valueKind someValue2 == Kind2

可能吗？

Answer 1

valueKind :: SomeValue a -> SomeKind不可能。 a类型参数不以任何形状或形式存在运行时，因此我们不能对其进行分支。

在运行时和编译时使用类型的标准方法是创建所谓的单例类型。单例由原始类型的类型级版本索引，并且具有我们可以通过对它们进行模式匹配来显示索引的属性:

data SSomeKind (i :: SomeKind) where
  SKind1 :: SSomeKind Kind1
  SKind2 :: SSomeKind Kind2

它们被称为单例，因为每个类型索引只有一个值。同样，对于每个值，类型索引只有一个选择。这种对应关系让我们可以使用 SSomeKind作为 SomeKind 的运行时表示.

valueKind' :: SSomeKind a -> SomeKind
valueKind' SKind1 = Kind1
valueKind' SKind2 = Kind2

创建单例定义和相关的升降功能是一项相当机械的工作。 singletons 库自动化和简化它。在我们的例子中:

{-# LANGUAGE TemplateHaskell, DataKinds, GADTs, TypeFamilies, ScopedTypeVariables #-}

import Data.Singletons.TH

$(singletons [d| data SomeKind = Kind1 | Kind2  |])
-- generates a lot of stuff, including the SSomeKind definition.

-- works the same as our previously defined function
valueKind' :: SSomeKind a -> SomeKind
valueKind' = fromSing

-- we can also polymorphically get specific singleton values:
foo :: Sing Kind1
foo = sing -- now foo equals SKind1

图书馆里还有很多。见 this page快速入门和进一步引用。