idris

3熱

1答えて

Idrisには有理数の既存の実装がありますか？など。 HaskellのData.Ratioポート。

3熱

1答えて

からIO`アクションは、与えられた `の評価： *lecture2> :let x = (the (IO Int) (pure 42)) は、その種類を見ると、MkFFI C_Types String String署名の意味は何ですか？ *lecture2> :t x x : IO' (MkFFI C_Types String String) Int 私はその後、REPLからxを評価しよ

26熱

1答えて

はidrisの型を含む型でインデックスされています

私は現在Type-Driven Development with Idrisの本を使っています。第6章では、サンプルデータストアの設計に関する2つの質問があります。データストアは、コマンドラインアプリケーションで、ユーザーはその中に格納されているデータの種類を設定して新しいデータを追加できます。ここにコードの関連部分を示します（わずかに簡略化）。あなたはGithubの上full codeを見る

1熱

1答えて

普通の再帰的なデータ型のインターフェイスを実装する

私はIdrisの構文と戦っているようです。 module Test data Nat = Z | S Nat Eq Nat where Z == Z = True S n1 == S n2 = n1 == n2 _ == _ = False これは、次のエラー（V1.1.1）で文句を言う： .\.\Test.idr:5:8: error: expected

4熱

1答えて

他の型をラップする型を表すWrapperインタフェース用の汎用ラップ関数を記述できますか？

下記の完全なコード例（正常にコンパイルされたもの）は、私の問題の単純化されたやや工夫された例です。 NatPairはNat秒のペアである、と私は機能lift_binary_op_to_pairを使用して「リフト」NatPair点ごとにバイナリNum操作、したいです。を実装することはできません。NatPairはデータコンストラクタではないためです。だから、私はタイプWrappedNatPairで

5熱

2答えて

入力タイプと出力タイプを同じにするにはどうすればよいですか？

私は、ManningのIdrisでタイプ駆動開発を行っています。型のファミリで関数を特定の型に制限する方法を教える例を示します。我々はPedalまたはPetrolのいずれかであるPowerSourceを使用するVehicleタイプを持っており、ガソリンをその電源として使用する車両についてのみタイプチェックを行うrefillという関数を書く必要があります。以下のコードは動作しますが、Carを補充す

6熱

4答えて

タイプのコンストラクタのサブセットのみを受け付ける関数を作成するにはどうすればよいですか？

だが、私はこのようなタイプがあるとしましょう： data Foo = Bar String | Baz | Qux String 私はこのような機能を持つようにしたい：欠落している場合があるように記述したよう get : Foo -> String get (Bar s) = s get (Qux s) = s を、これはコンパイルが、それはトータルではありません;言い換えれば、get

4熱

1答えて

lenとS lenを統一すると無限の値になる

同じ要素を必要な長さに達するまで繰り返すことによってhvectを生成する関数hpureを作成しようとしています。各要素は異なる型を持つことができます。例：引数がshowの場合、各要素はshow関数の特殊化になります。 hpure show : HVect [Int -> String, String -> String, SomeRandomShowableType -> String] これ

2熱

1答えて

Streamsの要素の完全性と検索

ListsとVectのfind関数に類似した、サイズに制限されたStreamsのストリームに対して、find関数が必要です。 total find : MaxBound a => (a -> Bool) -> Stream a -> Maybe a 課題は、それを作ることである。は Nが最大aを符号化するために必要なビット数であるせいぜい定数 log_2 Nスペースを消費しない合計です。