データプロモーション構文

https://stackoverflow.com//questions/24048620

21-12-2019
|

質問

最近発見したのは、 Data.Promotion 半分のシングルトン. 。型レベルで本質的に任意の計算を可能にする型ファミリーが多数あります。使用方法についていくつか質問があります。

違いは何ですか ($), (%$), ($$), 、そしてそれらは関連していますか？ :++$, :.$, 、など？これらは実際に中置演算子ですか?私はそうでした印象の下にすべての中置型コンストラクターは、 :.

コンストラクターをリストにマップしようとしています。

{-# LANGUAGE DataKinds, TypeOperators, PolyKinds #-}
import Data.Promotion.Prelude

data Foo a b
type MyList = '[Int, Double, Float]

 -- expects one more argument to `Foo`
type FooList1 b = Map ((Flip Foo) $ b) MyList

-- parse error on the second `b`
type FooList2 b = Map (($ b) :. Foo) MyList

しかし、マルチパラメータ型コンストラクタの使用に問題があります。アイデアは？

私が書いたすべての型関数を同等の関数に置き換えることができました。 Data.Promotion これを除いて：
```
type family ListToConstraint (xs :: [Constraint]) :: Constraint
type instance ListToConstraint '[] = ()
type instance ListToConstraint (x ': xs) = (x, ListToConstraint xs)
```
何か魔法がかかっているのでしょうか？ Constraint ネストされたペアとしての操作を防ぐような種類のものでしょうか?

解決

コメントで説明されているように、型レベルの中置関数がコロンで始まるという構文上の要件はなくなりました。はい、これらはすべて中置演算子です。2 つの中置演算子が自動的に相互に関連付けられることはありませんが、シングルトンライブラリは内部でいくつかの命名規則を使用して、使用されるシンボルを関連付けます。 非機能化 (下記を参照) 通常の対応物に。
型ファミリーは部分的に適用できないが、データ型は部分的に適用できるという事実から生じる問題は山ほどあります。そのため、シングルトンライブラリでは、と呼ばれる手法が使用されます。 非機能化:部分的に適用された型関数ごとに、データ型を定義します。次に、 (非常に大きくてオープンな) 型ファミリーがあります。 Apply これは、部分的に適用された関数と適切な引数を表すこれらすべてのデータ型を受け取り、実際のアプリケーションを実行します。

このような型関数の非関数化表現の種類は次のとおりです。
```
TyFun k1 k2 -> *
```
さまざまな理由からです (ところで、これについての詳しい紹介は、リチャード・アイゼンバーグのブログ投稿にあります) 「勝利のための非機能化」)、対応する「通常の」型関数の種類は次のようになります。
```
k1 -> k2
```
シングルトンのすべての高階型関数は、非関数化された引数を期待するようになりました。たとえば、次のような種類があります。 Map は
```
Map :: (TyFun k k1 -> *) -> [k] -> [k1]
```
そしてそうではありません
```
Map :: (k -> k1) -> [k] -> [k1]
```
次に、使用している関数を見てみましょう。
```
Flip :: (TyFun k (TyFun k1 k2 -> *) -> *) -> k1 -> k -> k2
```
最初の引数は、非関数化されたカリー化された種類の関数です。 k -> k1 -> k2, 、そしてそれはこれを一種の通常の型関数に変換します k1 -> k -> k2.

また：
```
($) :: (TyFun k1 k -> *) -> k1 -> k
```
これは単なる同義語です Apply 上で述べました。

次に、例を見てみましょう。
```
type FooList1 b = Map ((Flip Foo) $ b) MyList  -- fails
```
ここには 2 つの問題があります。初め、 Foo はデータ型であり、非機能化されたシンボルではありません。 Flip 期待しています。2番、 Flip は型ファミリーであり、3 つの引数が必要ですが、提供されるのは 1 つだけです。最初の問題は適用することで解決できます TyCon2, 、これは通常のデータ型を受け取り、それを非機能化されたシンボルに変換します。
```
TyCon2 :: (k -> k1 -> k2) -> TyFun k (TyFun k1 k2 -> *) -> *
```
2 番目の問題については、次の部分的な適用の 1 つが必要です。 Flip シングルトンはすでに次のように定義しています。
```
FlipSym0 :: TyFun (TyFun k1 (TyFun k2 k -> *) -> *)
                  (TyFun k2 (TyFun k1 k -> *) -> *)
            -> *
FlipSym1 ::    (TyFun k1 (TyFun k2 k -> *) -> *)
            -> TyFun k2 (TyFun k1 k -> *) -> *

FlipSym2 ::    (TyFun k1 (TyFun k2 k -> *) -> *)
            -> k2 -> TyFun k1 k -> *

Flip     ::    (TyFun k (TyFun k1 k2 -> *) -> *)
            -> k1 -> k -> k2
```
よく見てみると、 FlipSymN は、次の場合に必要な表現です。 Flip 部分的に適用される N 引数、および Flip 想像上のものに相当する FlipSym3. 。例では、 Flip は 1 つの引数に適用されるため、修正された例は次のようになります
```
type FooList1 b = Map ((FlipSym1 (TyCon2 Foo)) $ b) MyList
```
そしてこれは機能します:
```
GHCi> :kind! FooList1 Char
FooList1 Char :: [*]
= '[Foo Int Char, Foo Double Char, Foo Float Char]
```
2 番目の例も同様です。
```
type FooList2 b = Map (($ b) :. Foo) MyList
```
ここで、次の問題があります。また、 Foo を使用して非機能化シンボルに変換する必要があります TyCon2;演算子セクションなど $ b 型レベルでは使用できないため、解析エラーが発生します。使わなければなりません Flip またまた今度は FlipSym2, 、それを演算子に適用するため、 $ そして b. 。ああ、でもそれでは $ 部分的に適用されているため、に対応する記号が必要です。 $ 引数が0の場合。これは次のように利用可能です $$ シングルトン内 (シンボリック演算子の場合、非機能化されたシンボルが追加されています) $s）。そして最後に、 :. も部分的に適用されます。3 つの演算子が必要ですが、指定されているのは 2 つだけです。それで、私たちはから行きます :. に :.$$$ （1ドルが相当するので3ドル） 0, 、3ドルは以下に相当します。 2）。全体として：
```
type FooList2 b = Map ((FlipSym2 ($$) b) :.$$$ TyCon2 Foo) MyList
```
そして再び、これは機能します:
```
GHCi> :kind! FooList2 Char
FooList2 Char :: [*]
= '[Foo Int Char, Foo Double Char, Foo Float Char]
```
私は盲目かもしれませんが、これはシングルトンには含まれていないと思います。それはそれほど関係ありません Constraints.便利な機能なんですけどね。それは、私が現在取り組んでいるライブラリ. 。ただし、まだ未完成でほとんど文書化されていないため、まだリリースしていません。

ライセンス： CC-BY-SA と帰属

所属していません StackOverflow