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"

試みられた解決策

理想的には、この構造をトラバースして、 kind の値*に 1 対 1 のマッピングを返したいのですが、過負荷のために (必要な) インスタンスを持ち越しながら、これを異種混合で行う方法はあまり明白ではありません。

vanila on#haskellは、型クラスを使用して 2 つの世界をバインドすることを提案しましたが、思ったよりもややこしいようです。私の最初の試みは、インスタンス ヘッドの制約を介して型レベルのパターン マッチの内容をエンコードしようとしましたが、関連付けられた型 (*マッピングの -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は基本的に、タイプ andを提供する種類のクラスです。持ち上げられた値に対応する持ち上げられていない型を示します。たとえば、is ですが、isです。シングルトン値を対応するリフトされていない値に変換します。だから等しい。DemotefromSingDemoteDemote FalseBoolDemote "foo"SymbolfromSingfromSing SZZ

SingIリフトされた値をシングルトン値に反映するクラスです。singはそのメソッドでありsing :: Sing x、 のシングルトン値を提供しxます。これはほとんど私たちが望んでいるものです。の定義を完了するには、onreflectを使用して unlifted 値を取得するだけです。fromSingsing

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 aaはタイプではなく種類であるため、もちろん許可されません。したがって、右辺でKProxy使用できるようにするために必要です。a

日曜大工のソリューション

これはソリューションと同様に進みsingletonsますが、意図的にシングルトン表現をスキップして、直接リフレクションに進みます。これにより、パフォーマンスがいくらか向上するはずであり、その過程で少し学習することさえあるかもしれません (私は確かにそうしました!)。

import GHC.TypeLits
import Data.Proxy

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

kind ディスパッチをオープン型ファミリとして実装し、便宜上型シノニムを提供します。

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

一般的なパターンは'KProxy :: KProxy k、 kind について言及したいときにいつでも使用することです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 に答える