Отражение неоднородных продвигаемых типов обратно в значения композиционно

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 для значений вида *, но не очень очевидно, как сделать это неоднородно, все еще перенося (необходимые) экземпляры из-за перегрузки.

ваниль на #haskell предложил использовать классы типов, чтобы связать два мира, но это кажется немного сложнее, чем я думал. Моя первая попытка попыталась закодировать содержимое сопоставления с образцом на уровне типа через ограничение заголовка экземпляра, но мой связанный тип (для кодирования * -почвенный результат отображения) перекрывается - 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" []

И мы сделали.

К сожалению, библиотека редко документирована и довольно сложна. Я советую заглянуть на домашнюю страницу проекта для получения дополнительной документации. Я пытаюсь объяснить основы ниже.

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 нам нужно только использовать fromSing на 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))