問題タブ [uniqueness-typing]

クリーンでこれを行う方法は？

擬似コード:

実際、私はいくつかのpdfをちらっと見ました。でも、想像してみると、 stdin と stdout を扱うのは難しい。stdio を使用するコード例を教えてください。

キーランの指示に従って、私は小さなプログラムを完成させました。

UniqueTypeidris には、一度しか使用できない型の値と呼ばれる宇宙があります。私の知る限り、高性能コードの記述に使用できます。しかし、値が 1 回しか使用できないという事実は、通常はあまりにも制限されているため、値を消費する代わりに値を借用する方法があります。

Borrowedデータ型は Idris で上記のように定義されています。Type単純に戻らず、型の別の宇宙 ( BorrowedType)を導入するのはなぜですか?

Assuming I have *File that I want to read its whole content, and store each line as different element in a list.

My intuitive solution was:

Both freadline and fend come from StdFile module:

But ofcourse I got error since I violated some Uniquness rules:

file demanded attribute cannot be offerd by shared object.

How to avoid this Uniquness problem? I've tried using where to store the value of one freadline, but apparently it doesn't work.

Please consider the fact that I'm new to Clean and the rules of Uniqueness are not very clear to me. Thanks a lot!