[Agda] file for readFiniteFile

[Wolfram Kahl]

On Thu, Sep 22, 2016 at 03:48:36PM +0300, Sergei Meshveliani wrote:
> If you set 
>             12
> 
> into  data.txt,  the result string will have length 3.
> I guess that the last symbol is Newline, because this is visible on the
> screen output when running `main':
> 
>    ...> ./TT    
>    12 
>    ...>
> 
> instead of
> 
>    ...> ./TT    
>    12...>
> 
> I need to parse a number from the input string, and apply
> `initStr' (drop last character) to the string before parsing.
> (I doubt of whether this is a nice solution). 
> 
> My question was: how to obtain the input string without any parasitic
> last character and without any additional processing of the input
> string. 

It is not parasitic, it is just a character in the file.
Many people and editors consider text files not ending with a newline
character a bad idea.

Technically you should be able to produce a file that just contains
the two characters "12" --- try |writeFile "myfile" "12"| from GHC.

But if you want to rely on a special-purpose file format like that,
you have to be careful.

Better bite the bullet and use a parser.
(Haskell's |reads| functions are parsers, too...)


Wolfram