逆単射型家族

私の最初の質問は書くためにそこの方法ですT逆単射型家族

type family T a = b | b -> a

私は単射型家族がいるとしましょう：

type family T' = the inverse of T

Tのすべてのインスタンスを繰り返すことなく、しかし、逆に。

は、このようなこと：これは動作するはずのように両方TとT'が単射あるようT (X1 a (T' a)) = a

他を働かせて機械的である一方与えられた、と思われます。

とにかく書くにはT'？適した拡張子を持つ

2016-08-14 Clinton

なりません ' 〜T b'仕事？ – mb14

明らかに 'type Tinv b = a'は拒否されます。なぜなら' tinv'の引数にtyvar 'a'が記述されなければならないからです。 – chi

fundepを明示的な型のファミリアプリケーションに変換することは不可能ですが、@ mb14で述べたように、型シグネチャで等号制約を使用すると逆関数を計算できます。（a〜T b）=>プロキシa→プロキシb、または同等にはプロキシ（T b）→プロキシbである。 – user2407038

、1を書くことができます。たとえば

type T' b = forall a. T a ~ b => a

、ここでの例では、このタイプの同義語で、少なくとも基本的なタイプの互換性を得ることを示します：

type family T a = b | b -> a 
type instance T Int = Bool 

f :: T' Bool -> Int 
f x = x

2018-01-27 00:15:21

答えて