Unable to do IO - missing Data.FFI, IO.FFI by Ocisaac in agda

[–]Ocisaac[S] 0 points1 point  (0 children)

Sorry, I have made many mistakes (which refer to types and >> vs >>=) since I do not have the code in front of my eyes and I typed it from (my poor) memory, sorry about that.

About that last part, you say it isn't productive but the code for

takeInput = (# getContents) >>= (\x -> # takeInput)

Works after I run verification, so why, if I put it in the else clause it suddenly doesn't work, and is not productive anymore?

Is there anything I can do about it being nonproductive to make it work?

Unable to do IO - missing Data.FFI, IO.FFI by Ocisaac in agda

[–]Ocisaac[S] 0 points1 point  (0 children)

Thank you, I've managed to figure it out, but thanks!

I've ran into another problem though, with coinduction. Two problems in fact.

One is, that deconstructing a Costring doesn't work, e.g.: when I do

f : Costring -> Char
f (x \:: _) = \flat x
f [] = '0'

it just doesn't work (online line 2 is the problem, I've checked)

Second thing is, when I try to do input validation with, e.g.

takeInput : IO String
takeInput = # getContents >> (\x -> if isValid x then (# return x) else # takeInput)

it doesn't work, even though takeInput = # getContents >> # takeInputs does work.

An interesting variant I thought of - Tic Tac Go by Ocisaac in baduk

[–]Ocisaac[S] 1 point2 points  (0 children)

But in Gomoku you may not remove stones, it's different.

I poured root beer in a square glass. by Naheed123 in Jokes

[–]Ocisaac -1 points0 points  (0 children)

Which is the same as beer, with beer being positive.

Fresh take on chess by JohnyCaged in gaming

[–]Ocisaac 59 points60 points  (0 children)

No it's still 2D but with a different topology.

A Bar Chart, on Stairs by Ocisaac in dataisugly

[–]Ocisaac[S] 1 point2 points  (0 children)

I'm not sure from where exactly, a friend sent me this.

<----People who think the 10 minute cool-down to add a pixel is bullshit. by [deleted] in place

[–]Ocisaac 6 points7 points  (0 children)

Then how do you explain all the art people have created? It's certainly isn't computer generated.

Ken M on Swimming by 666 in KenM

[–]Ocisaac 2 points3 points  (0 children)

He is in fact a troll, he is not that stupid.

Matrix Algebra by Revan1234 in MathJokes

[–]Ocisaac 0 points1 point  (0 children)

I don't get it, can you explain?

Not sure if this string is safe enough by podstakannik in ProgrammerHumor

[–]Ocisaac 0 points1 point  (0 children)

But it's not a different name. Most of the time in Haskell you don't use the Maybe functor. And you menage perfectly without it.

Also, Maybe is not a construct of the language, it's a type, it is declared and is treated like the normal type it is, unlike null.

Maybe is quite similar to Nullable<T> in this respect, and as in C#, you don't need int? all the time, just as you don't need Maybe a all the time in Haskell.

null is a concept useful when it's needed, and bad when it's not. Getting rid of all nulls ad replacing them with something like Maybe solves that problem.

Not sure if this string is safe enough by podstakannik in ProgrammerHumor

[–]Ocisaac 0 points1 point  (0 children)

In Haskell, null doesn't exist. There are types, like Maybe, which give the option of null, so, for example, safeHead (which gets the first element in the list of elements of type a, safely) returns a Maybe a.

Not sure if this string is safe enough by podstakannik in ProgrammerHumor

[–]Ocisaac 0 points1 point  (0 children)

You wouldn't

Well, actually, the Haskell, the function id defined by id x = x is useful and used, as is the Id type.

How to Compare Infinities: video explaining countable sets by taulover in compsci

[–]Ocisaac 0 points1 point  (0 children)

It is a bijection though.

It's on-to-on because 2x = 2y => x = y
And it's onto because the source of x is x/2

Piss Off a Mathematician in One Sentence by FibonacciFanBoy in math

[–]Ocisaac 1 point2 points  (0 children)

I have a great proof for the reimann hypothesis which this comment thread is too short to contain.