When I gave my “Haskell Bytes” talk on the runtime representation of Haskell values the first time, I wrote here “It is in German, so [..] if you want me to translate it, then (convince your professor or employer to) invite me to hold the talk again“. This has just happened: I got to hold the talk as a Tech Talk at Galois in Portland, so now you can fetch the text also in English. Thanks to Jason for inviting me!
This was on my way to the Oregon Summer School on Programming Languages in Eugene, where I’m right now enjoying the shade of a tree next to the campus. We’ve got a relatively packed program with lectures on dependent types, categorical logic and other stuff, and more student talks in the evening (which unfortunately always collide with the open board game evenings at the local board game store). So at least we started to have a round of diplomacy, where I am about to be crushed from four sides at once. (And no, I don’t think that this has triggered the “illegal download warning” that the University of Oregon received about our internet use and threatens our internet connectivity.)
I am about to enter grad school in the next year and to this day, aside from using matlab to graph 3d functions, I still do math using pencil and paper. I am really interested in geometry and I just purchased a book on computational geometry. My main interests are differential geometry and topology. I would like to know how to get started in those areas using haskell.
I have looked at "haskell for great good" and I also own the book "The craft of functional programming". I have programmed in the past but I never really had a project that interested me so although I can program I don't do enough of it as I would like to.
Any good suggestions to some resources?submitted by spitfiredd
[link] [9 comments]
So I've just finished my final project at university, and i wanted to share it with you guys.
Source code is available here:
The task was to make an implementation of the applied pi-calculus. Its pretty rough around the edges, but it is functional.
If you just want to have a play around with the executable, its available on hackage as pi-calculus.
Any feedback or questions, I'll be happy to answer them.submitted by renzyq19
[link] [2 comments]
Philip Wadler: Research Funding in an Independent Scotland with Michael Russel, MSP and Cabinet Secretary
Much scaremongering has gone on around this subject and with this event we are hoping to meet the discussion head on to dispel fears and myths.
Also speaking will be Dr Stephen J Watson of the University of Glasgow and Chair of Academics For Yes who had an open letter on the subject printed in the Herald.
Anyone interested in the subject, Yes, Better Together, or Don't Know, is very welcome to attend. Questions from the audience on all topics related to the referendum will be invited in the Q&A. Please pass this on to anyone you think may be interested! This is a one-off opportunity from the Cabinet Secretary that we will not have again in the campaign.
WHEN 7-9pm Wednesday 25 June 2014
WHERE University of Edinburgh, JCMB Lecture Theatre B, Kings Campus
Edinburgh EH9 3JN
Google map and directions
CONTACT Dr Stephen J Watson · firstname.lastname@example.org · 07874233137
I have the following code:import System.Random (randomRIO) main :: IO () main = do putStr "Guess a number between 1 and 10: " n <- randomRIO (1, 10) :: IO Int loop n loop :: Int -> IO () loop n = do input <- getLine let g = read input :: Int if g < n then do putStr "Too low; guess again: " loop n else if g > n then do putStr "Too high; guess again: " loop n else do putStr "Correct!"
It seems to work, except for one minor (and when I say "minor" I mean "big") issue. The output happens after I have completed the game, and have already guessed the correct number. For example, the following is the contents of my terminal after completing the program:1 10 2 Guess a number between 1 and 10: Too low; guess again: Too high; guess again: Correct!
I'm sure this is due to haskells lazy evaluation. How can I make the print statements happen when I want them to?
Also, if anyone wants to critique the rest of my code, it would be appreciated.submitted by Buttons840
[link] [15 comments]
So, I'm going to say 'so' a lot in this post. You'll find out why this is, soonest.
soon, adv: composite word of the words 'so' and 'on.'
Amirite? Or amirite!
Today's 1HaskellADay challenge wasn't really a challenge, per se, so much as it was an observation, and that observation, keen as it might be...
keen, adj.: composite word of 'ki' (棋) and 'in' (院), transliteration from the Japanese: School of weiqi.
... was that the mapping function from one domain to a co-domain, and the corresponding co-mapping function from the co-domain to the domain gives you, when composed, the identity function in the domain or co-domain.
No, really! That was today's challenge.
To translate that into English:
f : a -> b
g : b -> a
(f . g) : a -> a
(g . f) : b -> b
So, we're not going to dwell on this, as Eilenberg and Mac Lane have dwelt on this so much better than I, but ...
Okay, so how do we prove this for our
CatA (being Either a a) and
CatB (being (Bool, a))?
With Haskell, it's easy enough, run your functions through quickcheck and you've got a PGP, that is: a pretty good (kinda) proof of what you want.
Or, you could actually prove the thing.
'You' meaning 'I,' in this particular case, and, while proving the thing, actually learn some me some more Idris for greater good.
Let's do that.
So, my last post have looked at a bit of proof-carrying code, and my methodology was to create a predicate that said whether some supposition I had held (returning a Bool, and, I hoped, True, at that!), unifying that with True, and then using the reflexive property of equality to prove that my supposition held.
Well, super neat, but today's problem was much harder for me, because I wrote something like this for one of my proofs:
leftIsomorphism : Eq a => (Bool, a) -> Bool
leftIsomorphism pair = (f . g) pair == pair
That, as far as it goes is just what we want, but when we try to prove it with this function:
isEqLeftTrue : Ea a => (val : a)
-> leftIsomorphism (True, val) = True
isEqLeftTrue val = refl
That doesn't work because of a type-mismatch, so replacing the predicate through substitution eventually lead to this type-error:
When elaborating right hand side of isEqLeftTrue:
x = x
(val : a) -> val == val = True
See, the problem (or, more correctly: my problem) is that
val == val
is true, but that's a property of boolean decidability, perhaps? It's easy enough to solve if I refine the term
val == val
then apply the reflexive property to obtain my proof, but the problem (again: my problem) is that I'm not all that savvy with refinement in proofs to get the answer out and blogged today.
The show must go on!
But the co-problem, or, getting a little less esoteric, the solution is that the Idris language already provides something that addresses this: so
Idris*> :t so
Prelude.Bool.so : Bool -> Type
With so we say that something is true, typefully, (that's a word, now) for us to proceed. So, our isEqLeftTrue, etc, functions become easy to write:
isEqLeftTrue : Eq a => (val : a)
-> so (leftIsomorphism (True, val)) -> ()
isEqLeftTrue val pred = ()
and then verification is simply the compilation unit, but you can query the type or test out any value with it as well:
Idris*> isEqLeftTrue "hey"
isEqLeftTrue "hey" : (so True) -> ()
And there you go, we've verified, for the left-adjoin anyway, that a (,) True type has the identity function. Let's verify the other three cases as well:
isEqLeftFalse : Eq a => (val : a)
-> so (leftIsomorphism (False, val)) -> ()
isEqLeftFalse val p = ()
... and for our right-adjoin proofs:
rightIsomorphism : Eq a => Either a a -> Bool
rightIsomorphism eith = (g . f) eith == eith
isEqRightLeft : Eq a => (val : a)
-> so (rightIsomorphism (Left val)) -> ()
isEqRightLeft val p = ()
isEqRightRight : Eq a => (val : a)
-> so (rightIsomorphism (Right val)) -> ()
isEqRightRight val p = ()
... and then the compilation proves the point, but we can exercise them, as well:
Idris*> isEqLeftFalse 1isEqLeftFalse 1 : (so True) -> ()
Idris*> isEqRightLeft 'a'isEqRightLeft 'a' : (so True) -> ()
Idris*> isEqRightRight "hey"isEqRightRight "hey" : (so True) -> ()
... and there you have it.
Huh. Looking at the above four proof-functions, they have the same type signatures (pretty much) and the same definitions. Hm. Maybe that's an indicator for me to start looking at Idris' syntactic extensions? Something for me to pensée about.
Ciao for now.
First of all let me point out that i'm new to haskell and it's entirely possible that I am doing something weird or silly. If that is the case do let me know ;-)
The other day I wanted to start working on a little tool that I had in mind and did not understand why hoogle would not find any of the functions belonging to a package that I was looking at. I finally realized that hoogle by default only indexes a base set of packages.
Info for all packages can be fetched using "hoogle data all". After that finally completed I was surprised because hoogle still did not find any of the functions i was interested in even though the hoogle database file of the package was clearly there.
So the only relevant package that is actually being searched is default.hoo and anything i want to search for has to be in there. For this purpose hoogle provides the "combine" command. This is where I reach a dead end.
TL;DR I can't figure out how to index all packages on hackage with hoogle. Is that such a weird thing to do ? The only other, even better thing I could think of would be separate hoogle databases per cabal project. That does not seem to exist though. I only found an issue with some discussion about it here
So how do you guys use hoogle then ?submitted by __gilligan
[link] [9 comments]