問題タブ [gadt]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
haskell - 関数 Int -> NatSing n を作成することは可能ですか?ここで、NatSing はペアノ番号のシングルトン タイプです。
漠然としたタイトルで申し訳ありません。ここにいくつかのコンテキストがあります：http://themonadreader.files.wordpress.com/2013/08/issue221.pdf
前号の GADTs の記事では、Nat 型と、さまざまな型レベルのリスト関数 (concat、!!、head、repeat など) で使用する NatSing 型を紹介しています。これらの関数のいくつかでは、Nat 型で + と < を定義するための型ファミリを作成する必要があります。
とにかく、呼び出し元の便宜のために、通常[a]を に変換する関数「リスト」を作成しました。これには、 （リンクされた記事から）のList n aように、入力としてリストの長さが必要です。repeat
ヘルパー関数を利用するとよいtoNatSing :: Int -> NatSing nので、上記は次のように記述できます。
そのような関数を書くことは可能toNatSingですか? 私は型と格闘してきましたが、まだ何も思いつきません。
どうもありがとう！
haskell - Haskell、GADT、および -fwarn-incomplete-patterns
私は Haskell で GADT の概念を取り上げようとしていて、Peano Number のシナリオに従おうとしていました。
しかし、これを-fwarn-incomplete-patternsフラグ (GHC-7.6.3) でコンパイルすると、考えられるすべてのパターンが用意されているにもかかわらず、次の警告が表示されます。
ただし、これらのパターンのいずれかに一致するものを含めると、次のようになります。
コンパイラは（正しくそうです）私に次のエラーを与えます：
基本的にこの関数のフラグを役に立たなくし、余分な醜いジャンクでコードを混乱させるtestFunc _ _ = undefined行を追加せずに、この関数またはデータ型を記述する方法はありますか?warn-incomplete-patterns
haskell - GADT で定義されたユニバーサル型からの変換を正しく定義できません
私は何でも含むことができる普遍的なデータ型を定義しました (まあ、現在の実装では完全に何もではありません)!
ここにあります（完全なコード）：
そして、コンソールで遊ぶことができます：
うーん、持ってるけど何とか加工しないと。たとえば、変換関数を定義しましょう (関数定義、前のコードに追加)。
そして、問題があります！前のコードのfromAny定義が正しくありません! そして、私はそれを正しくする方法がわかりません。GHCiでエラーが発生します：
エラーが発生する他の方法も試しました。
私はこれに対してかなり悪い解決策を持っています: showAnyTとreadを介して必要な関数を定義します(以前の関数定義を置き換えます):
はい、仕事です。私はそれで遊ぶことができます：
しかし、文字列を使用して変換するため、悪いと思います。
きちんとした良い解決策を見つけるのを手伝ってくれませんか?
haskell - この「似た形」のデータ型のペアでボイラープレートをどのように抽象化しますか?
一般的な質問
同じものを表す 2 つの異なる方法であるデータ型のペアがあります。1 つは String で変数名を記録し、もう 1 つは Int で変数名を記録します。現在、両方とも定義されています。ただし、ここでは最初の表現だけを説明したいと思います。2 つ目の表現は何らかの関係によって生成されます。
具体例
具体的には、最初のものは STLC ターム ユニバースのユーザー定義バージョンであり、2 つ目は同じものの de Bruijn インデックス付きバージョンです。
Termとに対して定義された関係が既に存在しTermInます:
Termの元の名前は に保存されているため、 とTermInの 1 対 1 のマッピングが存在することに注意してください。TermTermIn
質問を言い換える
Termこれでボイラー プレートがどれだけ関与しているかがわかります。これは、私が定義する洗練された抽象化と出力型に対する関数を使用して取り除きたいと考えていますTermIn。さらに多くのコンテキストを提供するために、さまざまなラムダ計算の定式化に対して、このような外部表現と de Bruijn 表現のペアを多数作成していますが、それらすべてに 1 対 1 の関係が成り立ちます。
haskell - Haskell でネストされたペアは良いアイデアですか
私の知る限り、Haskellで異種配列を実行したり、データ型を拡張したりする方法はありません。ただし、ネストされたペアを使用することで簡単に実現できるようです（CONSのように）。
例えば
このようにネストされたペアを使用して記述できます。
そうすれば、アクセサは Point2D と Point3D で共通にすることができます
このテクニックは、このようにレコードを拡張するためにも使用できます
など...
それは良い考えですか？それはGADTとは何ですか？