haskell - 以组合方式将异构提升类型反射回值

Question

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

背景

我想降级/反射(reflect)Strings 的简单玫瑰树, 成为 kind 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"

尝试的解决方案

理想情况下，我想遍历这个结构并将一对一的映射返回到类型 * 的值。 ，但是由于重载而仍然保留(必要的)实例的同时如何以异构方式执行此操作并不是很明显。

Vanilla #haskell建议我使用类型类来绑定(bind)两个世界，但这似乎比我想象的要复杂一些。我的第一次尝试尝试通过实例头约束对类型级别模式匹配的内容进行编码，但我的关联类型(用于编码映射的 * -kinded 类型结果)重叠 - 显然是 instance heads are somewhat ignored by 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是在飞行中。我不确定这目前是否无法编译，但我不相信这些类型会像我期望的那样统一。

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

Answer 1

懒惰的解决方案

安装 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" []

我们完成了。

不幸的是，该库的文档很少，而且也很复杂。我建议查看 project homepage一些额外的文件。我试图解释下面的基础知识。
Sing是定义单例表示的数据族。单例在结构上与未提升类型相同，但它们的值由相应的提升值索引。例如， data Nat = Z | S Nat 的单例将会

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

singletons是生成单例的模板函数(它还提升派生实例，也可以提升函数)。
SingKind本质上是一个类，它为我们提供了 Demote输入和 fromSing . Demote为我们提供了提升值的相应未提升类型。例如， Demote False是 Bool , 而 Demote "foo"是 Symbol . fromSing将单例值转换为相应的未提升值。所以 fromSing SZ等于 Z .
SingI是将提升的值反射(reflect)为单例值的类。 sing是它的方法， sing :: Sing x给我们 x 的单例值.这几乎就是我们想要的；完成 reflect的定义我们只需要使用 fromSing在 sing获得未提升的值(value)。
KProxy是 Data.Proxy 的导出.它允许我们从环境中捕获种类变量并在定义中使用它们。请注意，任何可推广的数据类型(* -> *)都可以用来代替 KProxy。 .数据类型提升详情 see this.

请注意，虽然种类上的调度形式较弱，但不需要 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))