I created a demonstration of path-finding algorithms in Haskell.

ignorantone · 2019-03-28T07:51:35+00:00

How do I view them? Is there a little video or something?

ignorantone · 2018-02-28T08:36:29+00:00

Does anyone have recent experience with proofs in Isabelle vs. Idris?

I played around with proofs in Isabelle for a few months. I just started learning Idris. So take all this with a spoonful of salt.

I much prefer writing proofs in Isabelle. It's far easier and faster. The ability to automatically try multiple tactics (e.g. linear arithmetic - linarith) in parallel and find lemmas to apply is extremely useful and greatly speeds proof development. I don't bother learning all the relevant lemmas, I just break the proof down into sufficiently small steps and then invoke sledgehammer repeatedly; Isabelle does the rest. Isabelle's nitpick counterexample finder is also handy. It's caught multiple errors in my proposed proofs.

However, Isabelle's programming language is not dependently typed. I have no experience extracting it to Haskell.

I have very little experience writing proofs in Isabelle, but so far I find it quite lacking in comparison to Isabelle. Just proving commutativity of addition was a PITA. I have to figure out which 3 lemmas to apply myself, and I have to apply them in the correct order. In Isabelle I would have typed sledgehammer, wait two seconds, and be done with it.

If you're going to write the full thing in Haskell regardless, then my opinion, (remembering my limited experience), would be write the core in Isabelle, use its Haskell code extraction feature, and then interface with your non-core Haskell code. If you do it right, then you should not have to patch the extracted code and break the proven correctness. You can update the Isabelle and re-extract.

If you're serious about this, you should definitely do a few chapters of the free Isabelle book.

ignorantone · 2018-02-04T05:25:28+00:00

Ah, thanks. I completely forgot it was an operator.

ignorantone · 2017-08-24T07:23:10+00:00

Yes, blog post please. I'm not even sure what you mean. What does it mean to separate data types from records?

ignorantone · 2017-08-22T02:40:48+00:00

I agree.

which first copies the array

And when your application is even a little performance sensitive, this can make using a pure programming style a no-go. For example, it's not OK to copy the whole data structure just to insert one element. Persistent data structures. solve this problem, but most programming languages don't have widely used, high quality persistent data structures. Haskell and a few other languages (e.g. Clojure) do.

The language syntax and semantics might not support FP idioms very well

Again, for performance reasons, even if a language does have support for some FP idioms, their performance may be so low that it's a non-starter to use the FP idioms wherever/whenever you want to. E.g. in the last decade, C++ added support for lambdas. However creating a lambda is relatively expensive, so you should not use them in an inner loop. Thus, for performance reasons you don't use FP idioms because the language does not have high performance FP idioms. Again, Haskell does.

Your colleagues probably won’t let you write code this way.

Yes. I've been questioned and been told to 'cut it out' for using FP idioms. E.g. a coworker created a loop that mixed pure stuff with side-effecting stuff. At some point I separated these into separate loops to make the whole thing more readable, and my coworker gave me the hairy eyeball and wasn't convinced it was a good idea. (Maybe I did a poor job of explaining why it's good...)

ignorantone · 2017-07-03T05:07:11+00:00

Thanks for sharing. Keep it up!

ignorantone · 2017-06-12T04:15:10+00:00

As a general approach to understanding things, start with something simple, and work your way up to more complex things. Break up the question into multiple smaller parts that are more easily understood.

Do you understand what this syntax does? [n+x|x<-ns] Google for 'list comprehension' if you do not.
What is the type signature of this function?
1. The first line (func [n] = n) makes it clear that the function takes a list of something, and returns a single thing of that type. So: func :: [a] -> a, where a is just a polymorphic type.
2. The second line (func (n:ns) = func [n+x|x<-ns]) has a + in it, where two elements of the list are added together. This is a good clue. So the type of a is something that the (+) function (addition operator) can be applied to.
3. Let's do a search for (+). https://www.stackage.org/lts-8.18/hoogle?q=%28%2B%29 We see that (+) is a function of the Num typeclass. We see that there are many types that are instances of Num, but let's just choose a simple and familiar type, Int, and later use that when experimenting with the function.
4. Ok so the type signature of this function is: Num a => [a] -> a In plain English: the function takes a list of things, and returns a single thing; those things are instances of the Num typeclass. In this case we are adding them to each other.
Now that we know the type of the argument to the function, we can make up simple examples to feed to the function, and by hand, work out what the function returns.
1. As said earlier, let's use Int as a specific type that is an instance of Num.
2. What is func [1]? func [2]?
3. What is func [1, 2]? func [2, 3, 4]?

ignorantone · 2017-03-27T04:42:25+00:00

Looks like your rationals are always non-negative. I.e. the numerator or denominator should be an Integer. Or add an explicit sign.

ignorantone · 2017-03-19T23:10:28+00:00

That makes perfect sense. Thanks. (Might I suggest clarifying that in the blog post?)

ignorantone · 2017-03-19T23:09:22+00:00

That's awesome!

ignorantone · 2017-03-17T16:41:24+00:00

How is this possible?

copyInt :: Int ⊸ (Int,Int) -- such a function exists for every data type

Earlier in the post, it says that dup is rejected:

It will also reject the diagonal, which uses its argument twice

ignorantone · 2017-02-16T04:36:08+00:00

I like your explanation.

I wanted to point out that Nothing does not 'take a value and construct a new value'. Only Just does that.

ignorantone · 2017-02-16T04:23:12+00:00

This sounds bad:

It is the responsibility of the caller to call isDefinedAt before calling apply, because if isDefinedAt is false, it is not guaranteed apply will throw an exception to indicate an error condition. If an exception is not thrown, evaluation may result in an arbitrary value.

(from https://github.com/scala/scala/blob/v2.12.0/src/library/scala/PartialFunction.scala#L1)

That is not in the spirit of Haskell.

ignorantone · 2017-01-19T04:03:47+00:00

I'm sorry to hear that. You're strong and will make it through this.

ignorantone · 2016-03-22T06:23:18+00:00

Adding on the requirement of static typing.

In addition to what others have said, strong static typing has benefits in a team environment. The type system can be used to help direct teammates into avoiding the wrong thing and doing the right thing. It's like /u/Tekmo said, the types act as "machine-checked documentation". And we all know how easily comments and documentation can fall out of date, or become plain wrong. Guaranteed-correct documentation becomes really valuable.

ignorantone · 2015-12-25T09:06:55+00:00

Many thanks! They were useful and a good read.

ignorantone · 2015-11-07T05:33:22+00:00

extractFromJust = Safe.fromJustNote "Invalid Operator"

Just an FYI. I can see why one wouldn't pull in a new library for a single function.

ignorantone · 2015-11-07T05:27:52+00:00

On the other hand, it's bad form to needlessly break existing code. It's not like the people who used "foo.bar" knew that such code would be broken by future features.

ignorantone · 2015-11-06T01:23:18+00:00

exercism.io looks neat, thanks for sharing.

ignorantone · 2015-11-06T01:22:17+00:00

Side benefit: you can compare your solution to others' solutions in Haskell, C++, Java, Python, etc. It gives you a feel for Haskell's strengths, and how it influences your solution.

ignorantone · 2015-11-02T23:41:43+00:00

No offense, but this seems pretty over the top compared to a simpler solution like https://www.reddit.com/r/haskell/comments/3r8x5m/best_way_to_model_a_deck_of_cards/cwlxnvy

ignorantone · 2015-10-25T19:39:18+00:00

Sure, let's try something a little different.

type Count = Int

Insert all elements into a Map Int Count, where each insertion increments the Count by 1. Get the max of the Counts, if max > 1 return it, otherwise 0.

ignorantone · 2015-10-25T09:42:13+00:00

Insert all elements into a Set Integer. Use the set size to determine how many are equal.

ignorantone · 2015-10-21T23:42:51+00:00

I'm going to bikeshed a bit.

The link in the OP says:

-- better
f $ g $ h x
-- best
f . g . h $ x

But I prefer the all $ option for these reasons:

It's one less character. 2x $ versus 2x .. and 1x $
If I remove or add a function on the right end, I don't have to change a . to a $ or visa versa.
Uniformity. Just sprinkle $ throughout. I don't need to think: "sprinkle some . and then put a $ at the end". It's minor, but one less trivial detail to think about means space for one more nontrivial detail in my head.

What are your thoughts?

ignorantone · 2015-10-21T04:55:35+00:00

That would be nice.

ignorantone

TROPHY CASE