News aggregator

Using Agda in Linux without emacs?

Haskell on Reddit - Tue, 07/08/2014 - 6:55pm

Hello, apologies if this question is irrelevant/doesn't belong here.
I've been reading a lot of agda tutorials for the past couple of days and almost all of them use emacs as an IDE (I might be wrong, but that's what it feels like). What I want to know is, can agda code be written separately and then afterwards be checked/compiled (again, not sure of the terminology) manually using commands in the terminal? I haven't been able to find much on the internet about this - any help at all would be very appreciated!

submitted by destsk
[link] [13 comments]
Categories: Incoming News

Danny Gratzer: Dissecting crush

Planet Haskell - Tue, 07/08/2014 - 6:00pm
Posted on July 9, 2014

For almost a year and half now I’ve been referencing one particular book on Coq, Certified Programming with Dependent Types. CPDT is a literate program on building practical things with Coq.

One of the main ideas of CPDT is that proofs ought to be fully automated. This means that a proof should be primarily a logic program (Ltac) which constructs some boring and large proof term. To this end, CPDT has a bunch of Ltac “tactics” for constructing such logic programs.

Since CPDT is a program, there’s actual working source for each of these tactics. It occurred to me today that in my 18 months of blinking uncomprehendingly at CPDT, I’ve never read its source for these tactics.

In this post, we’ll dissect how CPDT’s main tactic for automation, crush, actually works. In the process, we’ll get the chance to explore some nice, compositional, ltac engineering as well as a whole host of useful tricks.

The Code

The first step to figuring out of crush works is actually finding where it’s defined.

After downloading the source to CPDT I ran

grep "Ltac crush :=" -r .

And found in src/CpdtTactics, line 205

Ltac crush := crush' false fail.

Glancing at crush', I’ve noticed that it pulls in almost every tactic in CpdtTactics. Therefore, we’ll start at the top of this file and work our way done, dissecting each tactic as we go.

Incidentally, since CpdtTactics is an independent file, if you’re confused about something firing up your coq dev environment of choice and trying things out with Goal inline works nicely.

Starting from the top, our first tactic is inject.

Ltac inject H := injection H; clear H; intros; try subst.

This is just a quick wrapper around injection, which also does the normal operations one wants after calling injection. It clears the original hypothesis and brings our new equalities into our environment so future tactics can use them. It also tries to swap out any variables with our new equalities using subst. Notice the try wrapper since subst is one of those few tactics that will fail if it can’t do anything useful.

Next up is

Ltac appHyps f := match goal with | [ H : _ |- _ ] => f H end.

appHyps makes use of the backtracking nature of match goal with. It’ll apply f to every hypothesis in the current environment and stop once it find a hypothesis f works with.

Now we get to some combinators for working with hypothesis.

Ltac inList x ls := match ls with | x => idtac | (_, x) => idtac | (?LS, _) => inList x LS end.

inList takes a faux-list of hypothesis and looks for an occurrence of a particular lemma x. When it finds it we just run idtac which does nothing. In the case were we can’t match x anywhere, inList will just fail with the standard “No matching clause” message.

Next we have the equivalent of appHyps for tupled lists

Ltac app f ls := match ls with | (?LS, ?X) => f X || app f LS || fail 1 | _ => f ls end.

This works exactly like appHyps but instead of looking through the proofs environment, we’re looking through ls. It has the same “keep the first result that works” semantics too. One thing that confused me was the _ => f ls clause of this tactic. Remember that with our tupled lists we don’t have a “nil” member. But rather the equivalent of

A :: B :: C :: Nil

is

((A, B), C)

So when we don’t have a pair, ls itself is the last hypothesis in our list. As a corollary of this, there is no obvious “empty” tupled list, only one with a useless last hypothesis.

Next we have all, which runs f on every member in f ls.

Ltac all f ls := match ls with | (?LS, ?X) => f X; all f LS | (_, _) => fail 1 | _ => f ls end.

Careful readers will notice that instead of f X || ... we use ;. Additionally, if the first clause fails and the second clause matches, that means that either f X or all f LS failed. In this case we backtrack all the way back out of this clause. This should mean that this is a “all or nothing” tactic. It will either not fail on all members of ls or nothing at all will happen.

Now we get to the first big tactic

Ltac simplHyp invOne := let invert H F := inList F invOne; (inversion H; fail) || (inversion H; [idtac]; clear H; try subst) in match goal with | [ H : ex _ |- _ ] => destruct H | [ H : ?F ?X = ?F ?Y |- ?G ] => (assert (X = Y); [ assumption | fail 1 ]) || (injection H; match goal with | [ |- X = Y -> G ] => try clear H; intros; try subst end) | [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] => (assert (X = Y); [ assumption | assert (U = V); [ assumption | fail 1 ] ]) || (injection H; match goal with | [ |- U = V -> X = Y -> G ] => try clear H; intros; try subst end) | [ H : ?F _ |- _ ] => invert H F | [ H : ?F _ _ |- _ ] => invert H F | [ H : ?F _ _ _ |- _ ] => invert H F | [ H : ?F _ _ _ _ |- _ ] => invert H F | [ H : ?F _ _ _ _ _ |- _ ] => invert H F | [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H | [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H | [ H : Some _ = Some _ |- _ ] => injection H; clear H end.

Wow, just a little bit bigger than what we’ve been working with so far.

The first small chunk of simpleHyp is a tactic for doing clever inversion using the tuple list invOne.

invert H F := inList F invOne; (inversion H; fail) || (inversion H; [idtac]; clear H; try subst)

Here H is a hypothesis that we’re thinking about inverting on and F is the head symbol of H. First we run the inList predicate, meaning that we don’t invert upon anything that we don’t want to. If the head symbol of H is something worth inverting upon we try two different types of inversion.

In the first case inversion H; fail we’re just looking for an “easy proof” where inverting H immediately dispatches the current goal. In the second case inversion H; [idtac]; clear H; try subst, we invert upon H iff it only generates 1 subgoal. Remember that [t | t' | t''] is a tactic that runs t on the first subgoal, t’ on the second, and so on. If the number of goals don’t match, [] will fail. So [idtac] is just a clever way of saying “there’s only one new subgoal”. Next we get rid of the hypothesis we just inverted on (it’s not useful now, and we don’t want to try inverting it again) and see if any substitutions are applicable.

Alright! Now let’s talk about the massive match goal with going on in simplHyp.

The first branch is

| [ H : ex _ |- _ ] => destruct H

This just looks for a hypothesis with an existential (remember that ex is what exists desugars to). If we find one, we introduce a new variable to our environment and instantiate H with it. The fact that this doesn’t recursively call simplHyp probably means that we want to do something like repeat simplHyp to ensure this is applied everywhere.

Next we look at simplifying hypothesis where injection applies. There are two almost identical branches, one for constructors of two parameters, one for one. Let’s look at the latter since it’s slightly simpler.

| [ H : ?F ?X = ?F ?Y |- ?G ] => (assert (X = Y); [ assumption | fail 1 ]) || (injection H; match goal with | [ |- X = Y -> G ] => try clear H; intros; try subst end)

This looks for an equality over a constructor F. This branch is looking to prove that X = Y, a fact deducible from the injectiveness of F.

The way that we go about doing this is actually quite a clever ltac trick though. First we assert X = Y, this will generate to subgoals, the first that X = Y (shocker) and the second is the current goal G, with the new hypothesis that X = Y. We attempt to prove that X = Y by assumption. If this works, than we already trivially can deduce X = Y so there’s no point in doing all that injection stuff so we fail 1 and bomb out of the whole branch.

If assumption fails we’ll jump to the other side of the ||s and actually use injection. We only run injection if it generates a proof that X = Y in which case we do the normal cleanup with trying to clear our original fact and do some substitution.

The next part is fairly straightforward, we make use of that invert tactic and run it over facts we have floating around in our environment

| [ H : ?F _ |- _ ] => invert H F | [ H : ?F _ _ |- _ ] => invert H F | [ H : ?F _ _ _ |- _ ] => invert H F | [ H : ?F _ _ _ _ |- _ ] => invert H F | [ H : ?F _ _ _ _ _ |- _ ] => invert H F

Notice that we can now use the match to grab the leading symbol for H so we only invert upon hypothesis that we think will be useful.

Next comes a bit of axiom-fu

| [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H

inj_pair2 is function that lives in the Coq standard library and has the type

forall (U : Type) (P : U -> Type) (p : U) (x y : P p), existT P p x = existT P p y -> x = y

This relies on eq_rect_eq so it’s just a little bit dodgy for something like HoTT where we give more rope to = than just refl.

This particular branch of the match is quite straightforward though. Once we see an equality between two witnesses for the same existential type, we just generalize the equality between their proofs into our goal.

If this fails however, we’ll fall back to standard inversion with

| [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H

Finally, we have one last special case branch for Some. This is because the branches above will fail when phased with a polymorphic constructor

| [ H : Some _ = Some _ |- _ ] => injection H; clear H

Nothing exciting going on there.

So that wraps up simplHyp. It’s just a conglomeration of useful stuff to do to constructors in our hypothesis.

Onwards we go! Next is a simple tactic for automatically rewriting with a hypothesis

Ltac rewriteHyp := match goal with | [ H : _ |- _ ] => rewrite H by solve [ auto ] end.

like most of the other tactics we saw earlier, this will hunt for an H where this works and then stop. The by solve [auto] will run solve [auto] against all the hypothesis that the rewrite generates and ensure that auto solves all the new goals. This prevents a rewrite from going and introducing obviously false facts as goals for a rewrite that made no sense.

We can combine this with autorewrite with two simple tactics

Ltac rewriterP := repeat (rewriteHyp; autorewrite with core in *). Ltac rewriter := autorewrite with core in *; rewriterP.

This just repeatedly rewrite with autorewrite and rewriteHyp as long as they can. Worth noticing here how we can use repeat to make these smaller tactics modify all applicable hypothesis rather than just one.

Next up is an innocent looking definition that frightens me a little bit

Definition done (T : Type) (x : T) := True.

What frightens me about this is that Adam calls this “devious”.. and when he calls something clever or devious I’m fairly certain I’d never be able to come up with it :)

What this actually appears to do is provide a simple way to “stick” something into an environment. We can trivially prove done T x for any T and x but having this in an environment also gives us a proposition T and a ready made proof of it x! This is useful for tactics since we can do something like

assert (done SomethingUseful usefulPrf) by constructor

and viola! Global state without hurting anything.

We use these in the next tactic, instr.

Ltac inster e trace := match type of e with | forall x : _, _ => match goal with | [ H : _ |- _ ] => inster (e H) (trace, H) | _ => fail 2 end | _ => match trace with | (_, _) => match goal with | [ H : done (trace, _) |- _ ] => fail 1 | _ => let T := type of e in match type of T with | Prop => generalize e; intro; assert (done (trace, tt)) by constructor | _ => all ltac:(fun X => match goal with | [ H : done (_, X) |- _ ] => fail 1 | _ => idtac end) trace; let i := fresh "i" in (pose (i := e); assert (done (trace, i)) by constructor) end end end end.

Another big one!

This match is a little different than the previous ones. It’s not a match goal but a match type of ... with. This is used to examine one particular hypothesis’ type and match over that.

This particular match has two branches. The first deals with the case where we have uninstantiated universally quantified variables.

| forall x : _, _ => match goal with | [ H : _ |- _ ] => inster (e H) (trace, H) | _ => fail 2 end

If our hypothesis does, we randomly grab a hypothesis, instantiate e with it, add H to the trace list, and then recurse.

If there isn’t a hypothesis, then we fail out of the toplevel match and exit the tactic.

Now the next branch is where the real work happens

| _ => match trace with | (_, _) => match goal with | [ H : done (trace, _) |- _ ] => fail 1 | _ => let T := type of e in match type of T with | Prop => generalize e; intro; assert (done (trace, tt)) by constructor | _ => all ltac:(fun X => match goal with | [ H : done (_, X) |- _ ] => fail 1 | _ => idtac end) trace; let i := fresh "i" in (pose (i := e); assert (done (trace, i)) by constructor) end end end

We first chekc to make sure that trace isn’t empty. If this is the case, then we know that we instantiated e with at least something. If we have, we snoop around to see if there’s a done in our environment with the same trace. If this is the case, we know that we’ve done an identical instantiation of e before hand so we backtrack to try another one.

Otherwise, we look to see what e was instantiated too. If it was a simple Prop, we just stick a done record of this instantiation into our environment and add our new instantiated e back in with generalize. If e isn’t a proof, we do the same thing. In this case, however, we must also double check that the things we used to instantiate e with aren’t results of inster as well otherwise our combination of backtracking/instantiating can lead to an infinite loop.

Since this tactic generates a bunch of done’s that are otherwise useless, a tactic to clear them is helpful.

Ltac un_done := repeat match goal with | [ H : done _ |- _ ] => clear H end.

Hopefully by this point this isn’t too confusing. All this tactic does is loop through the environment and clear all dones.

Now, finally, we’ve reached crush'.

Ltac crush' lemmas invOne := let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in let rewriter := autorewrite with core in *; repeat (match goal with | [ H : ?P |- _ ] => match P with | context[JMeq] => fail 1 | _ => rewrite H by crush' lemmas invOne end end; autorewrite with core in *) in (sintuition; rewriter; match lemmas with | false => idtac | _ => (** Try a loop of instantiating lemmas... *) repeat ((app ltac:(fun L => inster L L) lemmas (** ...or instantiating hypotheses... *) || appHyps ltac:(fun L => inster L L)); (** ...and then simplifying hypotheses. *) repeat (simplHyp invOne; intuition)); un_done end; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)).

crush' is really broken into 3 main components.

First is a simple tactic sintuition

sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence

So this first runs the normal set of “generally useful tactics” and then breaks out some of first custom tactics. This essentially will act like a souped-up version of intuition and solve goals that are trivially solvable with straightforward inversions and reductions.

Next there’s a more powerful version of rewriter

rewriter := autorewrite with core in *; repeat (match goal with | [ H : ?P |- _ ] => match P with | context[JMeq] => fail 1 | _ => rewrite H by crush' lemmas invOne end end; autorewrite with core in *)

This is almost identical to what we have above but instead of solving side conditions with solve [auto], we use crush' to hopefully deal with a larger number of possible rewrites.

Finally, we have the main loop of crush'.

(sintuition; rewriter; match lemmas with | false => idtac | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); repeat (simplHyp invOne; intuition)); un_done end; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)).

Here we run the sintuition and rewriter and then get to work with the lemmas we supplied in lemmas.

The first branch is just a match on false, which we use like a nil. Since we have no hypothesis we don’t do anything new.

If we do have lemmas, we try instantiating both them and our hypothesis as many times as necessary and then repeatedly simplify the results. This loop will ensure that we make full use of bot our supplied lemmas and the surrounding environment.

Finally, we make another few passes with rewriter and sintuition attempting to dispatch our goal using our new, instantiated and simplified environment.

As a final bonus, if we still haven’t dispatched our goal, we’ll run omega to attempt to solve a Presburger arithmetic. On the off chance that we have something omega can be contradictory, we also try elimType false; omega to try to exploit such a contradiction.

So all crush does is call this tactic with no lemmas (false) and no suggestions to invert upon (fail). There you have it, and it only took 500 lines to get here.

Wrap Up

So that’s it, hopefully you got a few useful Ltac trick out of reading this. I certainly did writing it :)

If you enjoyed these tactics, there’s a more open-source version of these tactics, on the CPDT website. It might also interest you to read the rest of CpdtTactics.v since it has some useful gems like dep_destruct.

Last but not least, if you haven’t read CPDT itself and you’ve made it this far, go read it! It’s available as either dead-tree or online. I still reference it regularly so I at least find it useful. It’s certainly better written than this post :)

Note, all the code I’ve shown in this post is from CPDT and is licensed under ANCND license. I’ve removed some comments from the code where they wouldn’t render nicely with them.

<script type="text/javascript"> /* * * CONFIGURATION VARIABLES: EDIT BEFORE PASTING INTO YOUR WEBPAGE * * */ var disqus_shortname = 'codeco'; // required: replace example with your forum shortname /* * * DON'T EDIT BELOW THIS LINE * * */ (function() { var dsq = document.createElement('script'); dsq.type = 'text/javascript'; dsq.async = true; dsq.src = '//' + disqus_shortname + '.disqus.com/embed.js'; (document.getElementsByTagName('head')[0] || document.getElementsByTagName('body')[0]).appendChild(dsq); })(); </script> <noscript>Please enable JavaScript to view the comments powered by Disqus.</noscript> comments powered by Disqus
Categories: Offsite Blogs

Nottingham Research Fellowships

haskell-cafe - Tue, 07/08/2014 - 3:08pm
Dear all, The University of Nottingham is seeking applications for a number of Nottingham Research Fellowships: http://tinyurl.com/notts-fellows These are highly prestigious three-year fellowships, which are normally expected to lead into permenant academic positions. Candidates should have no more than 8 years postdoctoral experience, and fellowships normally start in October 2015. The deadline for submission of initial Expressions of Interest is ** 20th October 2014 **. Applicants in the area of the Functional Programming (FP) lab would be most welcome. The FP lab is keen to receive applications from outstanding candidates with an excellent publication record, experience in combining theory with practice, and the ability to secure external funding to support their research. Further information about the FP lab is available from http://fp.cs.nott.ac.uk As an approximate guideline, candidates in the area of the FP lab would normally be expected to have at least 3 years postdoc experience, and a nu
Categories: Offsite Discussion

Nottingham Research Fellowships

General haskell list - Tue, 07/08/2014 - 2:45pm
Dear all, The University of Nottingham is seeking applications for a number of Nottingham Research Fellowships: http://tinyurl.com/notts-fellows These are highly prestigious three-year fellowships, which are normally expected to lead into permenant academic positions. Candidates should have no more than 8 years postdoctoral experience, and fellowships normally start in October 2015. The deadline for submission of initial Expressions of Interest is ** 20th October 2014 **. Applicants in the area of the Functional Programming (FP) lab would be most welcome. The FP lab is keen to receive applications from outstanding candidates with an excellent publication record, experience in combining theory with practice, and the ability to secure external funding to support their research. Further information about the FP lab is available from http://fp.cs.nott.ac.uk As an approximate guideline, candidates in the area of the FP lab would normally be expected to have at least 3 years postdoc experience, and a n
Categories: Incoming News

Could this be done in Haskell?

Haskell on Reddit - Tue, 07/08/2014 - 12:38pm

Sorry for bad title, couldn't come up with a good one for this.

I was experimenting with an OOP style encoding of lists in Haskell. Not that I think it's a good idea (quite the opposite), but for fun.

A first attempt might look like this:

data List a = List { isEmpty :: Bool , head :: a , tail :: List a , map :: (a -> b) -> List b }

But this won't type check because the compiler don't know what b is. It should not be a parameter of List because that would not make sense. I think this might be right:

data List a = List { isEmpty :: Bool , head :: a , tail :: List a , map :: forall b.(a -> b) -> List b }

This requires the RankNTypes extension to compile. But I cannot define the list constructors:

nil = List { isEmpty = True , head = error "Empty list" , tail = error "Empty list" , map = const nil }

yields:

Couldn't match type ‘a’ with ‘b’ because type variable ‘b’ would escape its scope

I guess the problem is that nil in the definition of map recursivly refers to the nil we are defining.

Is this encoding possible somehow?

Also, is this what is called final encoding? (as opposed to the standard inital encoding for lists)

submitted by togrof
[link] [13 comments]
Categories: Incoming News

Which refinement types aren't structural?

Haskell on Reddit - Tue, 07/08/2014 - 10:47am

There seem to be two ways of encoding restrictions into types. One is via refinement types, we simply stick a predicate on top and prove it holds. The other way is to encode the restriction structurally. Sometimes we can do both, for example, we could encode an even number as a number with a proof of evenness, or directly as a datatype (DoubleThis Int). I have two conflicting intuitions here: One is that refinement types should be "less" than their full type, so there should be a lower information (structural) encoding. But on the other hand, if refinements are like subtraction (Type x, minus those that don't satisfy the predicate), then we could have "strictly negative" types with no physical representation.

Is there any classification of which (if any) refinement types do not admit a structural encoding?

(I suspect that those which admit a structural encoding are also those predicates which are "constructive", so we can encode them exactly as the witness)

submitted by dogirardo
[link] [4 comments]
Categories: Incoming News

[learn] Why isn't Integer an ADT?

Haskell on Reddit - Tue, 07/08/2014 - 8:00am

EDIT: this post is completely wrong, there are many good explanations in the comments.

It seems like this statement from the Haskell wiki is misleading:

An abstract data type is a type with associated operations, but whose representation is hidden. Common examples of abstract data types are the built-in primitive types in Haskell, Integer and Float.

That doesn't sound right. If Integer was an abstract data type with hidden constructors, you wouldn't be able to pattern match on it. But you can:

fac :: Integer -> Integer fac 0 = 1 fac n = n * fac (n - 1)

That said, the statement still sounds reasonable! If I were designing a Haskell-like language from scratch, I'd probably make Integer an ADT. That way you wouldn't be able to pattern match on it, and would have to use explicit comparisons, but everything else would work as expected.

Instead, it seems like Haskell chose to make Integer a sum type with infinitely many constructors, a special kind of type that users can't define for themselves. That leads to special cases in several places in the language. I'd like to understand, what was the rationale for that decision? What other useful things can you do with Integer as a sum type, that you can't do with Integer as an ADT?

A related question is why String is defined as [Char] instead of an ADT with appropriate operations. Maybe Haskell's designers were against using ADTs in the standard library for some reason?

submitted by want_to_want
[link] [27 comments]
Categories: Incoming News

Nottingham Research Fellowships

Haskell on Reddit - Tue, 07/08/2014 - 7:42am

The University of Nottingham is seeking applications for a number of Nottingham Research Fellowships:

http://tinyurl.com/notts-fellows

These are highly prestigious three-year fellowships, which are normally expected to lead into permenant academic positions. Candidates should have no more than 8 years postdoctoral experience, and fellowships normally start in October 2015. The deadline for submission of initial Expressions of Interest is ** 20th October 2014 **.

Applicants in the area of the Functional Programming (FP) lab would be most welcome. The FP lab is keen to receive applications from outstanding candidates with an excellent publication record, experience in combining theory with practice, and the ability to secure external funding to support their research. Further information about the FP lab is available from http://fp.cs.nott.ac.uk

As an approximate guideline, candidates in the area of the FP lab would normally be expected to have at least 3 years postdoc experience, and a number of strong publications in leading international venues such as ICFP, POPL, LICS, JFP, Haskell Symposium, etc.

Graham Hutton

submitted by grahamhutton
[link] [comment]
Categories: Incoming News

Job opening: further Haskell Developers at Anchor

haskell-cafe - Tue, 07/08/2014 - 7:21am
Openings for additional Haskell developers... About Anchor ------------ Anchor Systems, based in Sydney Australia, has successfully been providing managed hosting and infrastructure to clients around the world for almost 15 years. The critical difference in the service we offer our customers often boils down to providing operations expertise and infrastructure configuration balancing the short term needs to get a new installation running with the long term imperatives of security, scalability, and flexibility. The engineering department is building the analytics capabilities, internal systems, cloud infrastructure, deployment tooling, and operations practices that will be needed to take the company to the next level. We have every intention of changing the hosting industry to make developing applications — and operating them at scale — easier for people facing massive growth. Haskell is the working language for all internal development, and we're exploring it for web facing code too. The benefits of
Categories: Offsite Discussion

Using OpenGL inside a GTK notebook tab?

Haskell on Reddit - Tue, 07/08/2014 - 5:50am

Hello. I've been struggling with displaying an OpenGL drawing area inside of a notebook tab in GTK. What I need to do is to have two type of tab contents in my application: One is a text editor, using gtksourceview, which is used to write the input to a calculation procedure. When invoked, this procedure should do the calculation and then open a new notebook tab, which contains an OpenGL drawing area, displaying the results.

So far I just tried to get GL running by adapting the hello world example from the wiki. The thing is that it works fine when I put the drawing area into the main window when creating the main window in the first place, but it does not work properly when putting it in a notebook tab while the application is already running.

This is the basic outline of how I create my main window:

mainWindow :: IO () mainWindow = initGUI >> GtkGL.initGL >> goWin >> mainGUI goWin :: IO () goWin = do gui <- buildGUI connectGUI gui widgetShowAll $ window gui

Where buildGUI creates all the widgets that I need (returning them inside of a record) and connectGUI assigns signal handling to the individual widgets. No GL drawing area has been created yet. When pressing "calculate" in the menu, the calculations are done and a new ResultView is built as follows, which is then displayed in a new tab in the notebook:

buildResultView :: Either Result FilePath -> IO ResultView buildResultView d = do hbox <- hBoxNew False 0 glconfig <- GtkGL.glConfigNew [ GtkGL.GLModeRGBA , GtkGL.GLModeDepth , GtkGL.GLModeDouble ] gl <- GtkGL.glDrawingAreaNew glconfig Gtk.onRealize gl $ GtkGL.withGLDrawingArea gl $ \_ -> do clearColor $= (Color4 0.0 0.0 0.0 0.0) matrixMode $= Projection loadIdentity ortho 0.0 1.0 0.0 1.0 (-1.0) 1.0 depthFunc $= Just Less drawBuffer $= BackBuffers -- Set the repaint handler Gtk.onExpose gl $ \_ -> do GtkGL.withGLDrawingArea gl $ \glwindow -> do GL.clear [GL.DepthBuffer, GL.ColorBuffer] display GtkGL.glDrawableSwapBuffers glwindow return True boxPackStart hbox gl PackGrow 0 return $ ResultView hbox display = do loadIdentity color (Color3 1 1 0 :: Color3 GLfloat) -- Instead of glBegin ... glEnd there is renderPrimitive. renderPrimitive Polygon $ do vertex (Vertex3 1 0 0.0 :: Vertex3 GLfloat) vertex (Vertex3 1 1 0.0 :: Vertex3 GLfloat) vertex (Vertex3 0 1 0.0 :: Vertex3 GLfloat) vertex (Vertex3 0 0 0.0 :: Vertex3 GLfloat)

This is called by the following code, which builds the actual notebook tab:

newResultTab :: GUI -> Either Result FilePath -> IO () newResultTab gui d = do -- define tab label let lbl = either (const "<result>") takeFileName d fp = either (const Nothing) Just d -- build a new tab and resultview r <- buildResultView d tab <- buildNotebookTab (Right r) fp (Just lbl) -- wire close button onToolButtonClicked (ntCloseButton tab) $ do index <- notebookPageNum (nbook gui) (resultBox r) index ?>= \i -> notebookRemovePage (nbook gui) i -- add page widgetShowAll (resultBox r) menuLabel <- labelNew $ Just lbl index <- notebookAppendPageMenu (nbook gui) (resultBox r) (ntBox tab) menuLabel notebookSetTabReorderable (nbook gui) (resultBox r) True -- set as current and register modifyIORef (tabs gui) ((index,tab):) writeIORef (current gui) $ Just (index,tab) return ()

So my question is: The OpenGL code does clearly draw a yellow box, and it does actually do this when putting the drawing area into the main window at startup instead of the notebook. However, when I run it like above, all I get is a black window, and nothing is displayed in it. Does anyone have an idea how to fix this?

EDIT: I've got a minimal example of the problem which I've uploaded here.

submitted by tsahyt
[link] [4 comments]
Categories: Incoming News

Haskell Platform release schedule?

haskell-cafe - Tue, 07/08/2014 - 5:21am
The Haskell Platform wiki page says the platform follows a 6-month release schedule, yet the last release occurred more than one year ago, and I couldn't find information about future plans. Are there plans to update the platform with ghc 7.8.2? Thanks, Dominick
Categories: Offsite Discussion

Cross compiling for Cortex A9

glasgow-user - Tue, 07/08/2014 - 5:10am
I am having problems building a GHC cross compiler for Linux (Yocto on a Wandboard) running on a Cortex A9, and need some advice on how to debug it. The cross compiler produces an executable that runs on the Target, but fails to print. So I need help coming up with a strategy to narrow down the root cause. Some details: The application: main = do putStrLn "Haskell start" The command line options work. The program runs, and I can step through assembly. Debug data is printed to the console. But putStrLn fails, and program enters an infinite loop. I compile my app as follows: arm-unknown-linux-gnueabi-ghc -debug -static Main.hs Using -threaded does not fix the problem. Let me compare debug data from a run on my HOST, with a run on my TARGET. First, a run from my HOST: created capset 0 of type 2 created capset 1 of type 3 cap 0: initialised assigned cap 0 to capset 0 assigned cap 0 to capset 1 cap 0: created thread 1 cap 0: running thread 1 (ThreadRunGHC) cap 0: thread 1 stopped (suspended while m
Categories: Offsite Discussion

Machine learning through 'reflective metaprogramming.'

Haskell on Reddit - Tue, 07/08/2014 - 3:31am

Let's assume for the sake of argument some future time where computer algorithms are 'smart' enough to write their own code within a native source language or framework, then refactor and optimize that code, and basically add to their own programming to meet established goals or targets, which can themselves be modified and/or evolve with metaprogramming.

If this mythical machine existed and wrote code to modify its own programming, without concern at all for human readability or comprehension but instead purely for its own efficient design and function, then what language would it likely use in the most optimal scenario born out of current present day technologies?

  1. machine language
  2. assembly language
  3. C
  4. Lisp
  5. Haskell or ML variant
  6. Erlang
  7. Dynamic scripting language (Python, etc)
  8. Low level alternatives to C (D, Rust, Nimrod, etc)
  9. Other
submitted by RaymondWies
[link] [7 comments]
Categories: Incoming News

how to get ghci to load compiled modules in 7.8?

haskell-cafe - Mon, 07/07/2014 - 10:25pm
I recently upgraded to 7.8.2 and I have a silly question. How do you get ghci to load compiled modules? When I try this: % cat >T.hs module T where x :: Int x = 42 % ghc -c -dynamic-too T.hs % s T.dyn_hi T.dyn_o T.hi T.hs T.o % ghci GHCi, version 7.8.2: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer-gmp ... linking ... done. Loading package base ... linking ... done. Loading package filepath-1.3.0.2 ... linking ... done. Prelude> :l T [1 of 1] Compiling T ( T.hs, interpreted ) Ok, modules loaded: T. *T> It still loads the file interpreted, even though there is a .dyn_o present. What am I doing wrong? This is on x86-64 OS X.
Categories: Offsite Discussion

Where is Haskell going in industry?

Haskell on Reddit - Mon, 07/07/2014 - 3:13pm

I know this question may seem somewhat confrontational, but it's actually a thoughtful open letter from someone who really enjoys Haskell programming but whose day job unfortunately has involved lots of C++, Java, and Fortran programming throughout my career ( I work in games industry currently ).

Why is there is so much work on building more perfect languages and abstractions when the industry adoption already lags 25-30 years behind what you fellows are already working with?

I don't want to appear like I'm against progress in languages. I'm all for higher level and better abstractions and heated debates about extensional versus intensional type theory. But Haskell ( and FP on a larger scale ) seems to be of the "obelisk" model of design, seeing how high and far we can go, instead of the "pyramid" style of building out abstractions that can cover a larger area of use-cases.

For instance, there's a lot of bad C++ out there that is a giant imperative mess but covers enough of the industry use-cases, that network-effects tend to negate the use of anything better. I don't see anything replacing C++ for games programming on the order of the next 25 years and that scares me.

At least to me it appears the gap between the average industry programmer and the working Haskell developer is not shrinking but becoming insurmountably large. Even reading through Learn You a Haskell doesn't come close to preparing someone to read through half the libraries on Hackage. There's hundreds of languages extensions, types, and advanced patterns that seem to be ubiquitous but are not explained anywhere for the layman.

So my question to you fine Haskellers is how do you see Haskell getting more industry adoption and what can be done by folks like myself to help get there?

submitted by gamedevmike
[link] [112 comments]
Categories: Incoming News