問題タブ [injective-function]

Idris 言語チュートリアルには、従属型の考え方のシンプルでわかりやすい例があります: http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#first-class-types

コードは次のとおりです。

この例により多くの時間を費やすことにしました。関数で気になるのは、値を関数sumに明示的に渡す必要があることです。single : Bool私はこれをしたくありません。コンパイラに、このブール値がどうあるべきかを推測してもらいたいのです。したがって、関数のみを渡すかInt、ブール値と引数の型の間に 1 対 1 の対応がある必要があります (他の型を渡す場合、これは型チェックを行ってはなりません)。List Intsum

もちろん、これは一般的なケースでは不可能であることは理解しています。このようなコンパイラのトリックでは、関数isSingleton(または他の同様の関数) がinjectiveである必要があります。しかし、この場合、私には思えるように可能であるはずです...

そこで、次の実装から始めましたsingle。引数を暗黙的にしました。

さて、次の方法でこの関数を呼び出す必要があるため、実際には問題は解決しません。

sum {single=True} 1

しかし、autoキーワードに関するチュートリアルを読みました。何が機能するのかよくわかりませんautoが（説明が見つからなかったため）、関数にもう少しパッチを当てることにしました：

リストでも機能します。

しかし、単一の値では機能しません:(

現在、そのような単射関数の使用法で私の目標を達成することは実際に可能であることを誰かが説明できますか? 何かが単射であることの証明に関する短いビデオを見ました: https://www.youtube.com/watch?v=7Ml8u7DFgAk

しかし、私の例でそのような証明をどのように使用できるかわかりません。これが不可能な場合、そのような関数を作成する最良の方法は何ですか?

私はよく単射の写像を扱います。プログラミング用語では、これは、すべての値と、もちろんすべてのキーが一意である辞書として表現できます。

辞書から期待されるすべての時間の複雑さのプロパティを備えた単射マッピング用のメモリ効率の高いデータ構造はありますか?

例えば：

Two way/reverse mapのすべてのソリューションは、双方向マップで操作を実行しやすくすることに重点を置いて、2 セットのマッピングを使用または結合する必要があるようです。これは、メモリにきちんと収まる小さな辞書には適していますが、大きな辞書には適していません。

要件は、一方向マッピングのみを格納する通常のディクショナリに対して、単射双方向マップを格納する追加のメモリ オーバーヘッドがないことです。

辞書は、連想配列データ型を使用するハッシュ テーブルを使用することを理解しています。定義上、連想配列は一意のキーを使用してキー -> 値のマッピングを実装します。理論的または実際に、逆引きを可能にするスマートな単射マッピングを生成することは可能ですか?

不可能な場合は、辞書と同じ効率でそのような構成を実装することが難しい、または不可能である理由を説明していただければ幸いです。

アップデート

@rpy との議論に続いて (以下のコメントを参照)、完全な可逆ハッシュ関数を使用して Python 辞書のようなオブジェクトを設定する方法に関する情報は役に立ちます。しかし、もちろん、機能する実装が理想的です (私はすでに完全に試しました)。