News aggregator

How can I avoid this function to type-check?

Haskell on Reddit - Fri, 04/18/2014 - 1:41am

Notice that, on the program below, double_minus_one_is_even will never typecheck, independent of its input. How can I encode this so Haskell will report the problem before trying to apply that function to a value?

data Nat = Z | S Nat deriving (Show,Eq) is_nat :: Nat -> Nat is_nat Z = Z is_nat (S a) = S (is_nat a) is_even :: Nat -> Nat is_even Z = Z is_even (S (S a)) = (S (S (is_even a))) double :: Nat -> Nat double Z = Z double (S a) = (S (S (double a))) double_minus_one :: Nat -> Nat double_minus_one (S a) = S (double a) double_is_even :: Nat -> Nat double_is_even Z = Z double_is_even a = is_even (double (is_nat a)) double_minus_one_is_even :: Nat -> Nat double_minus_one_is_even Z = Z double_minus_one_is_even a = is_even (double_minus_one (is_nat a)) zero = is_nat Z one = is_nat (S Z) two = is_nat (S (S Z)) three = is_nat (S (S (S Z))) four = is_nat (S (S (S (S Z)))) main :: IO () main = print (double_minus_one_is_even two) {- Fails here, should fail before! -} submitted by SrPeixinho
[link] [62 comments]
Categories: Incoming News

Haskell Mode 13.07 - Thu, 04/17/2014 - 9:11pm
Categories: Offsite Blogs

A Haskell Compiler - Thu, 04/17/2014 - 1:39pm
Categories: Offsite Blogs

Product-ish class?

Haskell on Reddit - Thu, 04/17/2014 - 12:16pm

Is there already a class that looks like this, somewhere?

class P f where punit :: f () ppair :: f a -> f b -> f (a,b) phomotopy :: (a -> b) -> (b -> a) -> f a -> f b

Note that f doesn't need to be a Functor.

Update: added phomotopy

submitted by AshleyYakeley
[link] [29 comments]
Categories: Incoming News

C&C - Bargain Priced Coroutines - Thu, 04/17/2014 - 12:13pm
Categories: Offsite Blogs

Well-Typed.Com: Haskell gets static typing right

Planet Haskell - Thu, 04/17/2014 - 10:04am

The following blog post originally appeared as a guest post on the Skills Matter blog. Well-Typed are regularly teaching both introductory or advanced Haskell courses at Skills Matter, and we will also be running a special course on Haskell’s type system.

Statically typed languages are often seen as a relic of the past – old and clunky. Looking at languages such as C and Java, we’re used to writing down a lot of information in a program that just declares certain variables to be of certain types. And what do we get in return? Not all that much. Yes, granted, some errors are caught at compile time. But the price is high: we’ve cluttered up the code with noisy declarations. Often, code has to be duplicated or written in a more complicated way, just to satisfy the type checker. And then, we still have a significant risk of run-time type errors, because type casting is common-place and can fail at unexpected moments.

So it isn’t a big surprise that dynamically typed languages are now very fashionable. They promise to achieve much more in less time, simply by getting rid of static type checking.

However, I want to argue that we shouldn’t be too keen on giving up the advantages of static types, and instead start using programming languages that get static typing right. Many functional languages such as Scala, F#, OCaml and in particular Haskell are examples of programming languages with strong static type systems that try not to get in the way, but instead guide and help the programmer.

In the rest of this post, I want to look at a few of the reasons why Haskell’s type system is so great. Note that some of the features I’m going to discuss are exclusive to Haskell, but most are not. I’m mainly using Haskell as a vehicle to advertise the virtues of good static type systems.

1. Type inference

Type inference makes the compiler apply common sense to your programs. You no longer have to declare the types of your variables, the compiler looks at how you use them and tries to determine what type they have. If any of the uses are inconsistent, then a type error is reported. This removes a lot of noise from your programs, and lets you focus on what’s important.

Of course, you are still allowed to provide explicit type signatures, and encouraged to do so in places where it makes sense, for example, when specifying the interface of your code.

2. Code reuse

Nothing is more annoying than having to duplicate code. In the ancient days of statically typed programming, you had to write the same function several times if you wanted it to work for several types. These days, most languages have “generics” that allow you to abstract over type parameters. In Haskell, you just write a piece of code that works for several types, and type inference will tell you that it does, by inferring a type that is “polymorphic”. For example, write code that reverses all the elements of a data structure, and type inference will tell you that your code is independent of the type of elements of the data structure, so it’ll just work regardless of what element type you use. If you write code that sorts a data structure, type inference will figure out that all you require to know about the elements is that they admit an ordering.

3. No run-time type information by default

Haskell erases all type information after type checking. You may think that this is mainly a performance issue, but it’s much more than that. The absence of run-time type information means that code that’s polymorphic (i.e., type-agnostic, see above) cannot access certain values. This can be a powerful safety net. For example, just the type signature of a function can tell you that the function could reorder, delete or duplicate elements in a data structure, but not otherwise touch them, modify them or operate on them in any other way. Whereas in the beginning of this post I complained that bad static type systems don’t allow you to do what you want because they’re not powerful enough, here we can deliberately introduce restrictions to save us (as well as colleagues) from accidental mistakes. So polymorphism turns out to be much more than just a way to reduce code duplication.

By the way, Haskell gives you various degrees of selective run-time typing. If you really need it in places, you can explicitly attach run-time type information to values and then make type-based decisions. But you say where and when, making a conscious choice that you gain flexibility at the cost of safety.

4. Introducing new datatypes made easy

In Haskell, it’s a one-liner to define a new datatype with a new name that has the same run-time representation as an existing type, yet is treated as distinct by the type system. (This may sound trivial, but surprisingly many statically typed languages get it wrong.) So for example it’s easy to define lots of different types that are all integers internally: counters, years, quantities, … In Haskell, this simple feature is often used to define safe boundaries: a specific type for URLs, a specific type for SQL queries, a specific type for HTML documents, and so on. Each of these types then comes with specific functions to operate on them. All such operations guarantee that whenever you have a value of this type, it’s well-formed, and whenever you render a value of this type, it’s syntactically correct and properly escaped.

5. Explicit effects

In virtually all programming languages, a function that performs some calculations on a few numbers and another function that performs the same calculations, but additionally sends a million spam emails to addresses all over the world, have exactly the same type, and therefore the same interface. Not so in Haskell. If a function writes to the screen, reads from the disk, sends messages over the network, accesses the system time, or makes use of any other so-called side effect, this is visible in its type. This has two advantages: first, it makes it much easier to rely on other people’s code. If you look at the interface and a function is effect-free, then you for example automatically know that it is also thread-safe. Second, the language facilitates a design where side effects are isolated into relatively small parts of the code base. This may seem difficult to achieve for highly stateful systems, but surprisingly, it usually is not: even interactive systems can usually be described as pure functions reacting to a series of requests with appropriate responses, and a separate driver that does the actual communication. Such separation makes it not only easier to test the program, but also facilitates the evolution of the program such, for example, to adapt it to run in a different environment. Haskell’s type system therefore encourages good design.

6. Types as a guide in program development

If you only ever see types as a source of errors, and therefore as enemies on your path of getting your program accepted, you’re doing them injustice. Types as provided by Haskell are an element of program design. If you give your program precise types and follow systematic design principles, your program almost writes itself. Programming with a strong type system is comparable to playing a puzzle game, where the type system removes many of the wrong choices and helpfully guides you to take the right path. This style of programming is supported by a new language extension called “Typed Holes” where you leave parts of your program unspecified during development, and obtain feedback from the development environment about what type has to go into the hole, and what program fragments you have available locally to construct a value of the desired type. Playing this kind of puzzle game is actually quite fun!

7. Programming on the type level

Haskell’s type system provides many advanced features that you don’t usually have to know about, but that can help you if you want to ensure that some complicated invariants hold in your program. Scarily named concepts such as “higher-ranked polymorphism”, “generalized algebraic datatypes” and “type families” essentially provide you with a way to write programs that compute with types. The possibilities are nearly endless. From playful things such as writing a C-printf-style function where the first argument determines the number of arguments that are expected afterwards as well as their types, you can go on to code that provides useful guarantees such as that mutable references that are available within one thread of control are guaranteed not to be accessed in a completely different context, arrays that can adapt to different internal representations depending on what type of values they contain, working with lists that are guaranteed to be of a specific length, or with trees that are guaranteed to be balanced, or with heterogeneous lists (where each element can be of a different type) in a type-safe way. The goal is always to make illegal inputs impossible to construct. If they’re impossible to construct by the type system, you can isolate sanity tests at the boundary of your code, rather than having to do them over and over again. The good thing is that these features are mostly optional, and often hardly affect the interface of libraries. So as a user, you can benefit from libraries employing such features and having extra safety guarantees internally. As a library writer, you can choose whether you’re happy with the normal level of Haskell type safety (which is already rather a lot), or if you want to spend some extra effort and get even more.

If my overview has tempted you and you now want to learn more about Haskell, you’re welcome follow one of my introductory or advanced Haskell courses that I (together with my colleagues at Well-Typed) regularly teach at Skills Matter. These courses do not just focus on the type system of Haskell (although that’s a significant part). They introduce the entire language in a hands-on way with lots of examples and exercises, as well as providing guidelines on how to write idiomatic Haskell and how to follow good development practices.

If you already know some Haskell and are particularly interested in the advanced type system features mentioned in point 7, we also offer a new one-day course on Haskell’s type system that specifically focuses on how far you can push it.

Categories: Offsite Blogs

ZuriHac 2014 - Updates

Haskell on Reddit - Thu, 04/17/2014 - 6:26am
Categories: Incoming News

How to learn Haskell

Haskell on Reddit - Thu, 04/17/2014 - 5:37am
Categories: Incoming News

How do changes to the Haskell language/standard happen? How can I follow those changes?

Haskell on Reddit - Thu, 04/17/2014 - 12:37am

Having followed the Python community for quite awhile, I've appreciated the Python PEP's which give transparency to upcoming changes and ongoing discussions. Is there anything similar for Haskell?

I've found a few "clues" to start with thus far:

1) The Haskell wiki's "Proposals" page:

This page looks to me like a random collection of proposals, not a comprehensive collection. Some of the proposals have not been updated for many years.

2) Wikipedia's Haskell page:

According to Wikipedia: "In early 2006, the process of defining a successor to the Haskell 98 standard, informally named Haskell Prime, began.[25] This is an ongoing incremental process to revise the language definition, producing a new revision once per year. The first revision, named Haskell 2010, was announced in November 2009[1] and published in July 2010." That statement appears self contradictory. If a new revision is produced every year, why hasn't there been a new revision since 2010?

3) The current committee members:

I saw a posting on Reddit announcing the committee had been formed. It sounded nice, but I haven't heard any more about it? What does the committee do? Does the committee interact with the community? How can I follow what they are up to?

What's the best way to follow upcoming changes? How can I stay connected with the community who makes decisions regarding the language standard?

submitted by Buttons840
[link] [6 comments]
Categories: Incoming News

Douglas M. Auclair (geophf): 'N' is for No Nix Nada Nil Null Not Nothing

Planet Haskell - Thu, 04/17/2014 - 12:10am

'N' is for got Nuttin'!
I was thinking of covering the universal combinator, the Nightingale, with this post. It's a combinator that gives you any other combinator in the combinatory logic:
N = λx -> (xS)K
N = λx -> xKSK
or an infinite many other combinations of combinators that when combined repeatedly reduce either to the S or the K combinators, because the SK-basis has been shown to be Turing-complete.
But then I thought: eh! Maybe you've read enough about combinators this month, or to date, at any rate, so there is it: the N-combinator, the Nightingale, when combined with only itself (in certain desired ways), can give you any computable form. Yay!
So, let's talk about nothing for a sec here.
... hm, hm, hm, ...
Nice talk?
The problem with nothing is that there's nothing to talk about ... about it. But people tend to talk quite a bit, and if you reduce what they've just been saying to you and to everyone else who will listen (and quite a few of them won't), then you find that they haven't been really talking about anything at all, and, insult to injury, even they would find their own words boring, obnoxious, offensive, thoughtless, careless, if you played them back to them and forced them to listen to every word that came out of their mouths.
Ever listen to yourself speaking? Educational experience. Sometimes, I stop and listen to myself. Most times, I find, it would be better if I shut myself up sooner rather than later.
geophf, shut up! I tell myself.
Sometimes I listen when I tell myself that.
I feels better when I shut myself up when I'm speaking I have nothing to say
You know: THINK before you speak.

If it's not every one of those things, then why did I just open my mouth.
Here's another gauge.
Bad people talk about people.Good people talk about things.Great people talk about ideas and ideals.
What are you talking about?
Okay, but that's really 'something' that I've been talking about, and that is what people talk about, which is usually 'nothing good nor kind,' but it's still something, even if that something is vicious or inane or banal.
So let's talk about nothing.
The problem of nothing is that there's none of it. And here's why.
Get yourself to a pure vacuum. Is it inside a glass tube? No, because, actually, you've sucked most of the air out of it, but guess what? There's still quite a bit of light in there. That's not nothing. That's quite a bit of energy.
Drat! Bummer! So, turning off the night doesn't do anything for you. Visible light is gone but then you have infrared and ultravioletooh! vampires! — so you've got to go somewhere where's there's no light, no light, on either end of the visible spectrum.
Okay, spaaaaace!
Quite a lot of dust out there, star dust, and solar winds.
Hm, anywhere where we can go where there's nothing?
How about next to a black hole?
Now, that's interesting.
Now, if we can find a place somewhere around the black hole where it's not sucking up mass nor jetting out X-rays (and, granted, that would be hard to find, ... how about a black hole away from any nearby galaxy in spaaaace! Aw, the poor lonely black hole!) (Nobody cares about black holes being all alone, they're just like: oh! black hole! black holes are evil! I hate you, black hole! But does anybody ever consider the black hole's feelings when they're making these pronouncements? Noooo! They just say these things to the black hole's face, and then wonder why black holes are always so mean to them!)
There's still a problem. It's called the Hawking radiation.
You see, even in a 'pure vacuum' ... it isn't. Nature abhors a vacuum, so what happens is that there's so much energy around a black hole that it creates quantum particles (the Higgs field?) sucking most of them back into itself, but some little quarks escape, at around the speed of light (quark: 'Imma getting me away from that there black hole! NAOW!') and so Hawkings predicted, correctly, that even black holes emit radiation.
Bummer, dude! There doesn't seem to be anywhere where you can find yourself some nothing to be all sad and morose and all alone by yourself! You just have to buck up and accept the John Donne commandment: No quark is an island.
Or something like that.
BUT THEN! There's mathematics. You can invent a mathematical space where there's nothing in it, just it, and you (which makes it not nothing, but you get some quiet-time, finally, some alone time to catch up on your reading without having to worry about if the dishes were done).
What happens there? Besides nothing? What does it look like? Besides really, really empty?
Here's an interesting factoid (factoid, n.: geophf's interesting declarations that may or may not be somewhat related to some real reality), you're not the first visitor there.
There was this tall, thin dude in a white lab coat, by the name of Mach (no, not Mac the Knife, okay? Different Mac), and yes, the measure of velocity greater than the speed of sound was named after him (you know: mach 1, mach 2, mach 5+ for SR-71s), but besides that (and that's more than most people have ever done with their lives, but did he rest on his laurels? No. Besides, ... he still needed to earn his bread, so he could bake it, and then enjoy it with a latte) (lattes are important to physicists and mathematicians, don't you know.)
(But I digress.)
(As usual.)
Besides that, he did this thought-experiment. He created this mostly empty space, just him and the star Alpha Centauri in the distance. That was it in the entire Universe. And he spun himself, arms outstretched.
How did he know he was spinning? Easy, Alpha Centauri came into view, crossing it, then disappeared behind him as he spun, and he saw the star in an arc.
Next, he removed Alpha Centauri.
Now. Was he spinning?
He had no way to tell. You can tell you're spinning, because you get dizzy and then sick, but why? Because of gravity. Earth's gravity (mostly). But now there's not Earth.
There's not even Another Earth. So gravity is not now giving you a frame of reference, and you could tell you were spinning because there Alpha Centuri was in the distance, giving you your (only) point of reference, but now it's gone, too.
You could be moving a million miles per hour, you could be spinning and doing backward summersaults (or winter-saults for all you know: no seasons; no nothing. No nothing but nothing in your created Universe), and you'd have no frame of reference for you to make that determination.
Are you spinning in Mach's empty Universe?
The answer to that is: mu.
The answer to that question is that that's not a question to be asking. The answer to that question is that it has no sensible answer, whether you're spinning or not, you have no way to tell, or, no way to measure it. What's your coordinate system? How do you measure your speed or your spin. You don't, because if the XY-axis extends from in front of you, then it's always oriented to your front, no matter which way you face.
Anyway, where is time in all this? There's nothing. Space is bounded by the things in it, otherwise there's not space. 'Space' is emptiness, nothing there, but the space is defined by the no-thing between things.
There are no things in your nothing-Universe.
No space, no space-time. No space-time, no time. Spin needs time to measure.
If you had Alpha Centuri, then you would have light from four years ago shining on you, but now you have nothing, no light, no space, no time. No spin.
This post was about nothing, nothing at all. I hope you see when you get to that point where there is indeed nothing, no dust, no light, no nothing, you really, really do have nothing, not even space (the space between things: there are no things), not even time, not even spin.
Not even weight; weight needs gravity. You have no gravity in your nothing-Universe.
Enjoy the slim new-you, but the thing is, it'll be a lonely victory, so no bragging rights: nobody to brag to.
Okay, I'm going to go enjoy a latte with my busy, noisy family, and enjoy my not-nothing, not-solitude.
Nothing's not all cracked up to be what it's supposed to be.
Categories: Offsite Blogs

C++ Linking Woes

Haskell on Reddit - Wed, 04/16/2014 - 9:09pm
Categories: Incoming News

Web/Frameworks - HaskellWiki - Wed, 04/16/2014 - 8:45pm
Categories: Offsite Blogs

Autocomplete command line options with GHC 7.8

Haskell on Reddit - Wed, 04/16/2014 - 9:22am

GHC 7.8 adds --show-options flag that prints all supported command line flags on standard output. This can be used to enable autocompletion of command line options for ghc in shells that support autocompletion. If you're using bash add this snippet to your ~/.bashrc file:

# Autocomplete GHC commands _ghc() { local envs=`ghc --show-options` # get the word currently being completed local cur=${COMP_WORDS[$COMP_CWORD]} # the resulting completions should be put into this array COMPREPLY=( $( compgen -W "$envs" -- $cur ) ) } complete -F _ghc -o default ghc


PS. I also added a wiki page: Feel free to add instructions for other shells.

submitted by killy9999
[link] [10 comments]
Categories: Incoming News

Jan Stolarek: Autocomplete command-line flags with GHC 7.8.2

Planet Haskell - Wed, 04/16/2014 - 8:48am

GHC 7.8.2 has been released just a few days ago1. This is the first official release of GHC that contains my contributions. Most of them are improvements in the code generator and are thus practically invisible to most users. But I also implemented one very nice feature that will be useful to an average Haskeller. GHC now has --show-options flag that lists all command-line flags. This feature can be used to auto-complete command-line flags in shells that support this feature. To enable auto-completion in Bash add this code snippet to your ~/.bashrc file:

# Autocomplete GHC commands _ghc() { local envs=`ghc --show-options` # get the word currently being completed local cur=${COMP_WORDS[$COMP_CWORD]}   # the resulting completions should be put into this array COMPREPLY=( $( compgen -W "$envs" -- $cur ) ) } complete -F _ghc -o default ghc

From my experience the first completion is a bit slow but once the flags are cached things work fast.

  1. Please ignore 7.8.1 release. It shipped with a bug that caused rejection of some valid programs.
Categories: Offsite Blogs