Idris で String を Integer または Natural に変換する最良の方法は何ですか?
標準ライブラリはまだ進行中の作業であることを知っているので、答えが標準ライブラリに追加する必要がある場合は、それを試してみるのも問題ありませんが、まだ方法がないことを確認する前に.
ユーザーからインデックスを読み取りたい場合、私が思いつくことができる最善の方法は次のとおりです。
indexAsString <- getLine
let indexAsInt : Integer = cast indexAsString
let items: Vect _ _ = ["shoe", "bat", "hat"]
let i = integerToFin indexAsInt $ length items
maybe (print "invalid index") (\ii => print $ index ii items) i
しかし、この方法では、キャストからの失敗の兆候はありません。indexAsString が Integer に変換できる形式ではない可能性があるという事実だけでなく、実行時に失敗することさえなく、「不正なキャスト」の結果として 0 が生成されます。
より良い方法があることを教えてください、および/または正しい方向に向けてください。
余談ですが、Idris に Read 型クラスがない特別な理由はありますか? それともまだ入っていないだけですか？
事前にthx。