从结构上反映异构推广类型回到价值观

Question

我最近一直在玩-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映射回值类型的*,但不是很明显如何做到这一点不均匀,同时还携带,在(必要的)情况下,因超载.

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.我不确定目前是否会编译,但我不相信这些类型会像我期望的那样统一.

但是,这个类型类的heirarchy感觉是捕获异构语法的唯一方法,所以这可能仍然是一个开始.对此的任何帮助都将是巨大的!

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

我们已经完成了.

不幸的是,图书馆的文档很少,也非常复杂.我建议在项目主页上查看一些其他文档.我试着解释下面的基础知识.

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是一个将提升值反映为单值的类.sing是它的方法,并sing :: Sing x给我们的单例值x.这几乎是我们想要的; 完成定义reflect我们只需要使用fromSingon sing来获得未提升的值.

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)

我们将类型调度实现为开放类型系列,并为方便起见提供类型同义词:

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))