8

我最近一直在玩-XDataKinds，并想采用类型族的提升结构构建并将其拉回价值水平。我相信这是可能的，因为组合组件非常简单，终端表达式也很简单。

背景

我想降级/反映简单的玫瑰树Strings，它们成为一种类型Tree Symbol（当GHC.TypeLits.Symbol用作类型级字符串时）。这是我的样板代码：

{-# LANGUAGE DataKinds #-}

import GHC.TypeLits
import Data.Proxy

data Tree a = Node a [Tree a]

type TestInput = '[ 'Node "foo" '[ 'Node "bar" '[]
                                 , 'Node "baz" '[]
                                 ]
                  , 'Node "bar" '[]
                  ]

这是一个简单的类型级玫瑰森林，看起来像这个非常详细的图表：

 *-- "foo" -- "bar"
 |         \_ "baz"
  \_ "bar"

尝试的解决方案

理想情况下，我想遍历这个结构并将 1 对 1 映射回kind的值*，但是由于重载而仍然保留（必要的）实例的同时如何异构地执行此操作并不是很明显。

vanila on#haskell建议我使用类型类来绑定两个世界，但这似乎比我想象的要棘手。我的第一次尝试尝试通过实例头约束对类型级模式匹配的内容进行编码，但我的关联类型（用于编码*映射的 -kinded 类型结果）重叠 - 显然实例头在某种程度上被 GHC 忽略了。

理想情况下，我还希望列表和树的反射是通用的，这似乎会导致问题 - 这就像使用类型类来组织类型/种类层。

这是我想要的一个非功能示例：

class Reflect (a :: k) where
  type Result :: *
  reflect :: Proxy a -> Result

class ReflectEmpty (empty :: [k]) where
  reflectEmpty :: forall q. Proxy empty -> [q]
  reflectEmpty _ = []

instance ReflectEmpty '[] where

instance ReflectEmpty a => Reflect a where
  type Result = forall q. [q]
  reflect = reflectEmpty

-- | The superclass constraint is where we get compositional
class Reflect (x :: k) => ReflectCons (cons :: [x]) where
  reflectCons :: PostReflection x ~ c => Proxy cons -> [c]

instance ( Reflect x
         , ReflectCons xs ) => ReflectCons (x ': xs) where
  reflectCons _ = reflect (Proxy :: Proxy x) :
    reflectCons (Proxy :: Proxy xs)

instance ( Reflect x
         , ReflectEmpty e ) => ReflectCons (x ': e) where
  reflectCons _ = reflect (Proxy :: Proxy x) :
    reflectEmpty (Proxy :: Proxy e)

...

这段代码有几处通常是错误的。这是我看到的：

  • 我需要某种形式的前瞻来了解泛型类型级列表反射的更高种类反射的结果 -PostReflection类型函数
  • 我需要即时创建和销毁Proxy。我不确定这目前是否无法编译，但我不相信这些类型会像我期望的那样统一。

但是，这种类型类层次结构感觉像是捕获异构语法的唯一方法，所以这可能仍然是一个开始。对此的任何帮助都将是巨大的！

4

1 回答 1

8

懒惰的解决方案

安装singletons包：

{-# LANGUAGE
  TemplateHaskell, DataKinds, PolyKinds, TypeFamilies,
  ScopedTypeVariables, FlexibleInstances, UndecidableInstances, GADTs #-}

import GHC.TypeLits
import Data.Singletons.TH
import Data.Singletons.Prelude
import Data.Proxy

$(singletons [d|
  data Tree a = Node a [Tree a] deriving (Eq, Show)
  |])

reflect ::
  forall (a :: k).
  (SingI a, SingKind ('KProxy :: KProxy k)) =>
  Proxy a -> Demote a
reflect _ = fromSing (sing :: Sing a)

-- reflect (Proxy :: Proxy (Node "foo" '[])) == Node "foo" []

我们完成了。

不幸的是，该库的文档很少，而且也很复杂。我建议查看项目主页以获取一些其他文档。我试图解释下面的基础知识。

Sing是定义单例表示的数据族。单例在结构上与未提升类型相同，但它们的值由相应的提升值索引。例如，单例data Nat = Z | S Nat将是

data instance Sing (n :: Nat) where
  SZ :: Sing Z
  SS :: Sing n -> Sing (S n)

singletons是生成单例的模板函数（它还提升派生实例，也可以提升函数）。

SingKind本质上是一个kind 类，它为我们提供了Demotetype 和fromSing. Demote为我们提供了提升值的相应未提升类型。例如，Demote False是Bool，Demote "foo"而是Symbol。fromSing将单例值转换为相应的未提升值。所以fromSing SZ等于Z。

SingI是将提升的值反映为单例值的类。sing是它的方法，并sing :: Sing x为我们提供了 的单例值x。这几乎就是我们想要的；完成定义reflect我们只需要使用fromSingonsing就可以得到未提升的值。

KProxy是一个出口Data.Proxy。它允许我们从环境中捕获种类变量并在定义中使用它们。请注意，任何可推广的数据类型（* -> *）都可以用来代替KProxy. 有关数据类型提升的详细信息，请参阅此。

请注意，虽然种类上的调度形式较弱，但不需要KProxy：

type family Demote (a :: k)
type instance Demote (s :: Symbol) = String
type instance Demote (b :: Bool)   = Bool

到目前为止一切都很好，但是我们如何编写提升列表的实例呢？

type instance Demote (xs :: [a]) = [Demote ???]

Demote a当然是不允许的，因为a是一种，不是一种类型。所以我们需要KProxy为了能够a在右手边使用。

自己动手的解决方案

这与解决方案类似singletons，但我们故意跳过单例表示并直接进行反射。这应该更高效一些，我们甚至可以在这个过程中学到一些东西（我当然做到了！）。

import GHC.TypeLits
import Data.Proxy

data Tree a = Node a [Tree a] deriving (Eq, Show)

我们将 kind dispatch 实现为一个开放的类型族，并为方便起见提供了一个类型同义词：

type family Demote' (kparam :: KProxy k) :: *  
type Demote (a :: k) = Demote' ('KProxy :: KProxy k)

一般的模式是我们'KProxy :: KProxy k在想提及一种时使用k。 

type instance Demote' ('KProxy :: KProxy Symbol) = String
type instance Demote' ('KProxy :: KProxy (Tree a)) = Tree (Demote' ('KProxy :: KProxy a))
type instance Demote' ('KProxy :: KProxy [a]) = [Demote' ('KProxy :: KProxy a)]

现在进行反射非常简单：

class Reflect (a :: k) where
  reflect :: Proxy (a :: k) -> Demote a

instance KnownSymbol s => Reflect (s :: Symbol) where
  reflect = symbolVal

instance Reflect ('[] :: [k]) where
  reflect _ = []

instance (Reflect x, Reflect xs) => Reflect (x ': xs) where
  reflect _ = reflect (Proxy :: Proxy x) : reflect (Proxy :: Proxy xs)

instance (Reflect n, Reflect ns) => Reflect (Node n ns) where
  reflect _ = Node (reflect (Proxy :: Proxy n)) (reflect (Proxy :: Proxy ns))
于 2015-01-19T20:50:39.300 回答