idris

2熱

1答えて

タイプIntのタイプOrdの名前付き実装を定義しました。ので、別のモジュールで、私はこの実装をインポートする方法私は、この名前の実装をインポートし、「デフォルト」として使用することができます [mijnOrd] Ord Int where compare n1 n2 = ... マークそれをデフォルトとして、それを使用 - それはデフォルトたかのように sort [1,5,2]

4熱

1答えて

Idrisでは、IOはどの宇宙でも起こりうるのですか？

それは私の質問です。 Idrisには、宇宙がコンパイラによって推論される累積宇宙階層があります。 dosomethingreal : IOを使用すると、階層内の最低のユニバースが暗示されますか？ IO : Typeであり、決してIO : Type 1ですか？または、どの宇宙でもIOアクションを実行できますか？

2熱

1答えて

従属型

私は「ユニークなセールスポイント」が依存型のように見えるプログラミング言語Idrisに遭遇しました。どのような依存型があるのか、どのような問題に取り組んでいるのかを誰かが説明できますか？

1熱

1答えて

Idris：関数はNatパラメータで動作し、Integerパラメータで型検査に失敗します

Idrisを初めて使用しています。私は型を試しています。私の仕事は「玉ねぎ」を作ることです.2つの引数を取る関数です。数字と何でも入れて、何度も入れます。Listはそのような回数入れ子になっています。たとえば、mkOnion 3 "Hello World"の結果は[[["Hello World"]]]である必要があります。私はそのような機能を作った、これは私のコードです： onionListT

4熱

1答えて

平等のタイプを比較するには？

StringとStringを比較しようとしました.Trueと予想しています。 Idris> String == String Can't find implementation for Eq Type BoolにStringを比較する際それから私はFalseを期待。 Idris> String /= Bool Can't find implementation for Eq Type

1熱

1答えて

Vect n Nat's Evenlyの合計が5になるかどうかを判定しますか？

Cactus私の質問に対処する方法を示しました：Helper Function to Determine if Nat `mod` 5 == 0。彼が書いた： onlyModBy5 : (n : Nat) -> {auto prf : n `modNat` 5 = 0} -> Nat onlyModBy5 n = n をその後、私はVect n Nat年代の合計にonlyModBy5を適用

0熱

1答えて

2つの合計型を含むデータ型？</p> <pre><code>data Foo = A Int | B String data Bar = C Int | D String </code></pre> <p>私は<code>Either (Foo or Bar) String</code>を返す関数を定義したいと思います：

は、これら2種類の和を考えます。だから、私が作るしようとした： data Higher = Foo | Bar しかし、それはコンパイルに失敗しました： *ADT> :r Type checking ./ADT.idr ADT.idr:3:6:Main.Foo is already defined ADT.idr:4:6:Main.Bar is already defined どのよう

3熱

1答えて

インターフェイスの関数引数を制限する

関数を引数とするインターフェイスの関数引数を制約する構文は何ですか？ interface Num a => Color (f : a -> Type) where defs... をしかし、それはあなたのinterfaceName a is not bound in interface...

2熱

1答えて

Idrisインターフェイスで関数型を制約する

インターフェイスで制約された型の関数を作成したいと思います。私の目的は、VerifiedMonoidをClasses.Verifiedのcontribパッケージから定義して、単純なモノイドソルバーを構築することです。 eval : VerifiedMonoid a => Expr n -> Env a n -> a 私は愚かな何かをするか、何かが欠けています：evalの型シグネチャのため Mo

0熱

2答えて

リストの平等は、この演習を提示イドリスと

型駆動開発を機能定義：私は「ので、私はEqList (x :: xs) (x :: ys)でxを推論 data EqList : (xs : List a) -> (ys : List a) -> Type where Same : (xs: List a) -> EqList xs xs sameS : (xs : List a) -> (ys : List a) -> (x: a