9

異種リストを分析する関数を書きたいと思います。議論のために、次のようにしましょう

data Rec rs where
  Nil :: Rec '[]
  Cons :: ty -> Rec rs -> Rec ( '(name, ty) ': rs )

class Analyze name ty where
  analyze :: Proxy name -> ty -> Int

最終的な目標は、次のようなものを書くことです

class AnalyzeRec rs where
  analyzeRec :: Rec rs -> [(String, Int)]

instance AnalyzeRec '[] where
  analyzeRec Nil = []

instance (Analyze name ty, AnalyzeRec rs) => 
           AnalyzeRec ( '(name, ty) ': rs ) 
  where
    analyzeRec (Cons hd tl) = 
      let proxy = Proxy :: Proxy name
      in (symbolVal proxy, analyze proxy hd) : analyzeRec tl

analyzeRecの各タイプと値でインスタンス化された制約の知識を使用する顕著なビットRecです。このクラスベースのメカニズムは機能しますが、これを何度も行わなければならない場合 (私もそうしています) は、扱いにくく冗長です。

singletonsしたがって、代わりにこれを に基づくメカニズムに置き換えたいと思います。代わりに次のような関数を書きたい

-- no type class!
analyzeRec :: All Analyze rs => Rec rs -> [(String, Int)]
analyzeRec rec = 
  case rec of
    Nil -> []
    Cons hd tl -> withSing $ \s -> 
      (symbolVal s, analyze s hd) : analyzeRec tl

しかし、これは明らかに少なくともいくつかの次元で横ばいです。

シングルトン手法を使用して、異種リストに対してそのような関数を記述する「正しい」方法は何ですか? この問題にアプローチするより良い方法はありますか? この種のことを解決するには、何を期待すればよいですか?

(参考までに、これは Serv と呼ばれる実験的な Servant クローン用です。関連するファイルは背景としてServ.Internal.Header.Serializationあります。タグ付けされたヘッダー値の異種リストを取り込み、それらを実際のペアのリストに入れるServ.Internal.Header関数を書きたいと思います。 )headerEncode(ByteString, ByteString)

4

2 に答える 2

4

ここでは、「慣用的な」singletons解決策を提示しようとします (そのようなものが存在する場合)。予選:

{-# LANGUAGE
  RankNTypes, DataKinds, PolyKinds, ConstraintKinds, GADTs,
  TypeOperators, MultiParamTypeClasses, TypeFamilies, ScopedTypeVariables #-}

import Data.Singletons.Prelude
import Data.Proxy
import GHC.Exts (Constraint) 

-- SingI constraint here for simplicity's sake
class SingI name => Analyze (name :: Symbol) ty where
  analyze :: Proxy name -> ty -> Int

data Rec rs where
  Nil :: Rec '[]
  Cons :: ty -> Rec rs -> Rec ( '(name, ty) ': rs )

recName :: Rec ('(name, t) ': rs) -> Proxy name
recName _ = Proxy

制約が必要ですが、All c rsそれにスピンを与えてc、TyFun代わりに単純なa -> Constraintコンストラクターを作成します。

type family AllC (c :: TyFun a Constraint -> *) (rs :: [a]) :: Constraint where
  AllC c '[]       = ()
  AllC c (x ': xs) = (c @@ x, AllC c xs)

TyFun型コンストラクターと型ファミリーを抽象化し、部分的な適用を可能にします。これにより、構文がいくぶん見苦しい、ほとんどファーストクラスの型レベル関数が得られます。ただし、必然的にコンストラクターの注入性が失われることに注意してください。-s@@を適用するための演算子です。それが入力であり出力であることを意味し、末尾は単なるエンコーディングのアーティファクトです。GHC 8.0 でできることTyFunTyFun a b -> *ab-> *

type a ~> b = TyFun a b -> *

そしてa ~> bその後も使用。

これで、次の一般的な「上品な」マッピングを実装できますRec。

cMapRec ::
  forall c rs r.
  AllC c rs => Proxy c -> (forall name t. (c @@ '(name, t)) => Proxy name -> t -> r) -> Rec rs -> [r]
cMapRec p f Nil           = []
cMapRec p f r@(Cons x xs) = f (recName r) x : cMapRec p f xs

上記cには kind があることに注意してくださいTyFun (a, *) Constraint -> *。

そして実装しますanalyzeRec：

analyzeRec :: 
  forall c rs. (c ~ UncurrySym1 (TyCon2 Analyze)) 
  => AllC c rs => Rec rs -> [(String, Int)]
analyzeRec = cMapRec (Proxy :: Proxy c) (\p t -> (fromSing $ singByProxy p, analyze p t))

1つ目は、略記としてinを使用できるc ~ UncurrySym1 (TyCon2 Analyze)型レベルのletバインディングです。(すべての汚いトリックを本当に使用したい場合は、 を追加して記述します)。cProxy c{-# LANGUAGE PartialTypeSignatures #-}Proxy :: _ c

UncurrySym1 (TyCon2 Analyze)uncurry AnalyzeHaskell が型レベル関数を完全にサポートしていた場合と同じことを行います。analyzeRecここでの明らかな利点は、余分なトップレベルの型ファミリやクラスなしでその場での型を書き出すことができ、AllCさらにはるかに一般的に使用できることです。

SingIおまけとして、から制約を取り除き、Analyzeを実装してみましょうanalyzeRec。

class Analyze (name :: Symbol) ty where
  analyze :: Proxy name -> ty -> Int

nameここで、すべての-s が であることを表す追加の制約を要求する必要がありRecますSingI。cMapRec2 つの-sを使用して、結果を圧縮できます。

analyzeRec ::
  forall analyze names rs.  
  (analyze ~ UncurrySym1 (TyCon2 Analyze),
   names   ~ (TyCon1 SingI :.$$$ FstSym0),
   AllC analyze rs,
   AllC names rs)
  => Rec rs -> [(String, Int)]
analyzeRec rc = zip
  (cMapRec (Proxy :: Proxy names)   (\p _ -> fromSing $ singByProxy p) rc)
  (cMapRec (Proxy :: Proxy analyze) (\p t -> analyze p t) rc)

ここでTyCon1 SingI :.$$$ FstSym0は として翻訳できますSingI . fst。

TyFunこれは、 -sで簡単に表現できる抽象化のレベルの範囲内です。もちろん、主な制限はラムダがないことです。zipを使用する必要はなく、代わりに をAllC (\(name, t) -> (SingI name, Analyze name t))使用し、単一の を使用するのが理想的cMapRecです。ではsingletons、ポイントフリーの型レベル プログラミングでこれ以上うまくいかない場合は、新しいポイントフル型ファミリを導入する必要があります。

面白いことに、GHC 8.0 は十分に強力なので、型レベルのラムダをゼロから実装することができますが、それはおそらく地獄のように醜いものになるでしょう。たとえば、\p -> (SingI (fst p), uncurry Analyze p)次のようになります。

Eval (
  Lam "p" $
    PairL :@@
      (LCon1 SingI :@@ (FstL :@@ Var "p")) :@@    
      (UncurryL :@@ LCon2 Analyze :@@ Var "p"))

ここで、すべてのL接尾辞は、通常の -s のラムダ項の埋め込みを示しますTyFun(TH によって生成されるさらに別の短縮形のコレクション...)。

私はプロトタイプを持っていますが、GHC のバグのため、さらに醜い de Bruijn 変数でしか動作しません。Fixまた、型レベルでの明示的な遅延も特徴としています。

于 2015-12-21T21:36:50.427 に答える