News aggregator

Do you recognize this type?

haskell-cafe - Thu, 06/19/2014 - 4:17pm
Hi guys, I am making a DSL for event composition (inspired from digestive-functor & reactive-banana) and I find myself wanting a primitive like that:
Categories: Offsite Discussion

Joachim Breitner: Another instance of Haskell Bytes

Planet Haskell - Thu, 06/19/2014 - 2:00pm

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.)

Categories: Offsite Blogs

Relations between Functor typeclass and kind

haskell-cafe - Thu, 06/19/2014 - 8:36am
Hi all, Some days ago, I was talking with someone about Kinds and GADTs. At some point he mention that types with this Kind: (* -> *) are called Functors. So, is there any relations between Functor typeclass and Functor kind? Is it considered as a "pattern"? if so, are there some other ones? If you have any link on this, I'll take them. Thanks in advance for your help. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Categories: Offsite Discussion

How do use haskell to do math research?

Haskell on Reddit - Thu, 06/19/2014 - 6:37am

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]
Categories: Incoming News

Applied pi-calculus interpreter written in Haskell

Haskell on Reddit - Thu, 06/19/2014 - 6:34am

So I've just finished my final project at university, and i wanted to share it with you guys.

Source code is available here:

https://github.com/renzyq19/pi-calculus

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]
Categories: Incoming News

diagrams

haskell-cafe - Thu, 06/19/2014 - 4:31am
I'm a math tutor and I want to create videos to explain certain math concepts, and I'm wondering if the diagrams library would help me. There are two questions--first, whether it has the capability to do what I want, and second how hard it would to integrate the animations into YouTube videos with voice-over. To describe the capability, I'm looking first to typeset equations. Then, second, to represent manipulation of equations by having elements of equations move locations or cross-fade. Also "elements" could mean pictures or non-mathematical notation. I have no doubt that diagrams can make the diagrams themselves. What I wonder about is the animation capabilities---ability to have elements move or cross-fade (dissolve), in particular. As far as the ability to integrate these into YouTube videos, that is probably beyond the scope of this list, but maybe someone happens to have done this and knows the answer. Mike _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >hask
Categories: Offsite Discussion

Philip Wadler: Research Funding in an Independent Scotland with Michael Russel, MSP and Cabinet Secretary

Planet Haskell - Thu, 06/19/2014 - 2:53am
MICHAEL RUSSELL MSP, CABINET SECRETARY FOR EDUCATION AND LIFE LONG LEARNING is coming 7-9pm Wednesday 25 June to the University of Edinburgh to speak on the issue of Research Funding in an Independent Scotland.
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
Mayfield Road
Edinburgh EH9 3JN
Google map and directions

CONTACT Dr Stephen J Watson · scienceforscotland@gmail.com · 07874233137
Categories: Offsite Blogs

Haskell Weekly News: Issue 297

haskell-cafe - Thu, 06/19/2014 - 2:08am
Welcome to issue 297 of the HWN, an issue covering crowd-sourced bits of information about Haskell from around the web. This issue covers from June 8 to 14, 2014 Quotes of the Week * dpwright: this afternoon I've literally taken an entire (portrait) screen's worth of code and reduced it to about three lines and a few lens operators * tommd: Haskell is a great language. I needed to test a program under high CPU load, so to burn some cycles I cabal-installed lens. Is there anything Haskell can't do? * bernalex: I imagine hell as a place where spj & edwardk are holding talks at the same time and I have to choose. Top Reddit Stories * Haxl on Github Domain: github.com, Score: 124, Comments: 25 Original: [1] http://goo.gl/zw8Y8q On Reddit: [2] http://goo.gl/FoV1zw * www.dohaskell.com Domain: dohaskell.com, Score: 92, Comments: 23 Original: [3] http://goo.gl/uxmtUy On Reddit: [4] http://goo.gl/xkGJUb * cloud-haskell is on hackage now
Categories: Offsite Discussion

[Newb Question] Why isnt' my guess number game working?

Haskell on Reddit - Wed, 06/18/2014 - 10:16pm

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]
Categories: Incoming News

dead links on mailing list page

haskell-cafe - Wed, 06/18/2014 - 8:40pm
I was trying to look at some mailing list archives, and encountered several dead links in section 1.3 on this page: http://www.haskell.org/haskellwiki/Mailing_lists - 3rd paragraph, link to http://www.cse.unsw.edu.au/~dons/haskell-1990-2006/threads.html (a 403 is returned), where the link is under the text "hosted here" - 4th paragraph, link to the Google Coop Haskell Search Engine (a 404 is returned) I wasn't sure where else to report this. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Categories: Offsite Discussion

Douglas M. Auclair (geophf): oh : so True

Planet Haskell - Wed, 06/18/2014 - 5:44pm
So, ...

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!

SO!

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

Wowsers!

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:

Can't unify
x = x
with
(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 

down to

True

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.
Pensée
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.
Categories: Offsite Blogs

ANNOUNCE: haste-perch

General haskell list - Wed, 06/18/2014 - 3:02pm
Hi, haste-perch defines builder elements (perchs) for Haste.DOM elements that are appendable, so that dynamic HTML can be created in the client in a natural way, like textual HTML, but programmatically and with the advantage of static type checking. It can be ported to other haskell-js compilers. http://hackage.haskell.org/package/haste-perch This program, when compiled with haste: main= do withElem "idelem" $ build $ do div $ do div $ do p "hello" p ! atr "style" "color:red" $ "world" return () Creates these element: <div id= "idelem"> <-- was already in the HTML <div> <div> <p> hello </p> <p style= "color:red"> world </p> </div> </div> </div> Since the creation is in the browser, that permit quite dynamic pages for data presentation, and interctive textual (a.k.a "serious") applications and, in general the development of client-side web frameworks using haskell with the haste compiler. See the
Categories: Incoming News

Banging my head against the wall with hoogle

Haskell on Reddit - Wed, 06/18/2014 - 2:29pm

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.

I have tried the shell script described at local-install.md and also rehoo. Both to no avail. Both will either fail somewhat silently or run into an error for which I filed an issue here: hoogle

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]
Categories: Incoming News