如何将数据类型带入价值水平？

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

图书馆里还有很多东西.请参阅此页面以获取快速入门和进一步参考.

Answer 2

如果您可以容忍类型类约束,则可以使用每种类型的实例来完成此操作SomeKind.这与Kindable类型类非常相似

class SomeKindable (k :: SomeKind) where
    someKindOf :: p k -> SomeKind

instance SomeKindable Kind1 where
    someKindOf _ = Kind1

instance SomeKindable Kind2 where
    someKindOf _ = Kind2

valueKind ::  SomeKindable a => SomeValue a -> SomeKind
valueKind = someKindOf

编译器不能告诉所有人k :: SomeKind都有一个SomeKindable k实例.如果您需要将此功能提供给每个人SomeValue而无法显示SomeKindable,则可以将值与SomeKindable字典一起打包GADT.

{-# LANGUAGE GADTs #-}

data SomeValue (t :: SomeKind) where
    SomeValue :: SomeKindable t => SomeValue t

valueKind :: SomeValue a -> SomeKind
valueKind (p@SomeValue) = someKindOf p

Answer 3

您可以定义一个类型类,该类型类基于type-parameter返回关联的值.

class ValueKind (t :: SomeKind) where
    valueKind :: f t -> SomeKind

instance ValueKind Kind1 where
    valueKind _ = Kind1

instance ValueKind Kind2 where
    valueKind _ = Kind2