# News aggregator

### Any Haskell-OpenGL tutorial including shader compilation, buffer usage and so on?

Does anyone who has already worked with Haskell's OpenGL library know if there is a tutorial including shader compilation, uploading buffers and so on? If not, what is your approach to using OpenGL's lib? What documentation are you using, and how do you link its information to the lib (the high-level wrapper, not the raw bindings).

Thanks!

submitted by SrPeixinho[link] [28 comments]

### ghc -O2 out of memory

### -staticlib flag for building standalone static libraries producing very large libraries

### Philip Wadler: A paean to the Western General

I resided in Ward 42 of the Regional Infectious Disease Unit of Edinburgh's Western General Hospital from 17 Dec—2 Jan. For most of the time I received antibiotic by drip or injection every four hours, day and night, and I thought my stay would be six weeks. Fortunately, my infection reacted well to antibiotic and I could be released early for outpatient treatment.

The building is ugly, but the people inside it are beautiful. I cannot recall another time or place where everyone was so unfailingly helpful and friendly. On the first day, a nurse found a staff member willing to lend me a charger when my phone ran down. The doctors took as much time as needed to answer my questions. The nurses were cheerful despite constant interruptions. The men who brought the coffee remembered that I liked it with milk, and one often asked after my twins (he had twins as well). No one objected when my daughter brought me a poster of the Justice League and I blue-tacked to my wall; several admired it.

Most often, I interact with institutions where the people who help you are, clearly, in it for the pay. They are nice only to the extent required by their job, and often less than that. Part of the difference in attitude here must be that the people know they are actively helping patients in need. I take my hat off to an institution that inculcates a caring attitude in everyone.

(Picture above courtesy of The Edinburgh Sketcher, whose pictures adorn a couple of corridors in the Western General. The RIDU is a different building, though somehow every building in the complex contrives to be equally unattractive.)

**Related**: Status report, Status report 2.

### A step by step tutorial for a Web Framework

I've been learning Haskell and would like to have a go at actually writing something I can use. I've worked through LYAH and read several other tutorials and books. Unfortunately I can't find a step by step, explanative tutorial for any of the web frameworks. There is the Yesod book but it didn't give me a good foundation for building something of my own.

I'm looking for something akin to this (Python, Pyramid).

Is there anything like this written already?

Cheers

submitted by Teifion[link] [26 comments]

### Principled Casts in Haskell (Beginner)

### SPDX and hackage

### Data.Graph (and Data.Tree) improvements

### drKraken/haskell-must-watch

### Danny Gratzer: Worlds in Twelf

In this post I wanted to focus on one particular thing in Twelf: %worlds declarations. They seems to be the most mysterious. I’ve had a couple people tell me that they just blindly stick %worlds () (x _ _ _) before every total and pray which is a little concerning..

In this post hopefully we’ll remove some of the “compile-n-pray” from using Twelf code.

What is %worldsIn Twelf we’re interested in proving theorems. These theorems are basically proven by some chunk of code that looks like this.

my-cool-tyfam : with -> some -> cool -> args -> type. %mode my-cool-tyfam +A +B +C -D. some : ... -> my-cool-tyfam A B C D. constructors : ... -> my-cool-tyfam A B C D. %worlds (...) (my-cool-tyfam _ _ _ _). %total (T) (my-cool-tyfam T _ _ _).What’s interesting here is the 3 directives we needed

- %mode to specify which arguments of the type family are universally quantified and which are existentially qualified in our theorem. This specifies the “direction” of the type family, + arguments are inputs and - arguments are outputs.
- %total which actually goes and proves the theorem by induction on the canonical forms of the term in the parens.
- %worlds which specifies the set of contexts to check the totality in. Note that a world is simply a set of contexts.

The one we’re interested in talking about here is %worlds. Everything we want to call %total has to have on of these and as mentioned above it specifies the contexts to check the theorem in. Remember that total is proven by induction over the canonical forms. One of the canonical forms for every type is off the form

For some x : ty ∈ Γ, then x is a canonical form of ty.

This is a little different than in other languages. We could usually just invert upon something in the context. That’s not the case in Twelf, we have to handle variables parametrically (this is critical to admitting HOAS and similar). This means that means we have to extremely careful about what’s in Γ lest we accidentally introduce something canonical form of ty without any additional information about it. The worlds specification tells us about the forms Γ can take. Twelf allows us to specify sets of contexts that are “regular”.

So for example remember how plus might be defined.

plus : nat -> nat -> nat -> type. %mode plus +N +M -P. plus/z : plus z N N. plus/s : plus N M P -> plus (s N) M (s P).This is total in the empty context. If we added some b : nat to our context then we have no way of showing it is either a s or a z! This means that there’s a missing case for variables of type nat in our code. In order to exclude this impossible case we just assert that we only care about plus’s totality in the empty context. This is what the %worlds specification for plus stipulates

%worlds () (plus _ _ _).should be read as “plus should only be considered in the empty context” so the only canonical forms of plus are those specified as constants in our signature. This sort of specification is what we want for most vanilla uses of Twelf.

For most cases we want to be proving theorems in the empty context because we do nothing to extend the context in our constructors. That’s not to say that we *can’t* specify some nonempty world. We can specify a world where there is a b : nat, but if such a b must appear we have a derivation {a} plus b a z. This way when Twelf goes to check the canonical forms case for something in our context, b : nat, it knows that there’s a derivation that precisely matches what we need. I’ll circle back to this in a second, but first we have to talk about how to specify fancier worlds.

In Twelf there’s some special syntax for specifying worlds. Basically we can specify a template for some part of the world, called a block. A world declaration is just a conglomeration of blocks and Twelf will interpret this as a world of contexts in which each block may appear zero or more times.

In Twelf code we specify a block with the following syntax

%block block_name : block {a : ty} ... {b : ty'}.This specifies that if there is an a : ty in the context, it’s going to be accompanied by a bunch of other stuff including a b : ty'. Some blocks are pretty trivial. For example, if we wanted to allow plus to be defined in a context with some a : nat in the context we might say

%block random_nat : block {b : nat}. %worlds (random_nat) (plus _ _ _).This doesn’t work though. If we ask Twelf to check totality it’ll get angry and say

Coverage error --- missing cases: {#random_nat:{b:nat}} {X1:nat} {X2:nat} |- plus #random_nat_b X1 X2.In human,

You awful person Danny! You’re missing the case where you have to random integers and the random natural number b from the random_nat block and we want to compute plus b X X'.

Now there are a few things to do here. The saner person would probably just say “Oh, I clearly don’t want to try to prove this theorem in a nonempty context”. *Or* we can wildly add things to our context in order to patch this hole. In this case, we need some proof that about adding b to other stuff. Let’s supplement our block

Such a context is pretty idiotic though since there isn’t a natural number that can satisfy it. It is however enough to sate the totality checker.

%total (T) (plus T _ _).For a non contrived for example let’s discuss where interesting worlds come into play: with higher order abstract syntax. When we use HOAS we end up embedding the LF function space in our terms. This is important because it means as we go to prove theorems about it we end up recursing on a term *under* an honest to goodness LF lambda. This means we extend the context at some points in our proof and we can’t just prove theorems in the empty context!

To see this in action here’s an embedding of the untyped lambda calculus in LF

term : type. lam : (term -> term) -> term. app : term -> term -> term.Now let’s say we want to determine how many binders are in a lambda term. We start by defining our relation

nbinds : term -> nat -> type. %mode nbinds +T -N.We set this type family up so that it has one input (the term) and one output (a nat representing the number of binders). We have two cases to deal with here

nbinds/lam : nbinds (lam F) (s N) <- ({x : term} nbinds (F x) N). nbinds/app : nbinds (app F A) O <- nbinds F N1 <- nbinds A N2 <- plus N1 N2 O.In the lam case we recurse under the binder. This is the interesting thing here, we stick the recurse call under a pi binder. This gives us access to some term x which we apply the LF function two. This code in effect says “If for all terms F has N binders then lam F has N + 1 binders. The app case just sums the two binders.

We can try to world check this in only the empty context but this fails with

Error: While checking constant nbinds/lam: World violation for family nbinds: {x:term} </: 1This says that even though we promised never to extend the LF context we did just that! To fix this we must have a fancier world. We create a block which just talks about adding a term to the context.

%block nbinds_block : block {x : term}. %worlds (nbinds_block) (nbinds _ _).This world checks but there’s another issue lurking about. Let’s try to ask Twelf to prove totality.

%total (T) (nbinds T _).This spits out the error message

Coverage error --- missing cases: {#nbinds_block:{x:term}} {X1:nat} |- nbinds #nbinds_block_x X1.This is the same error as before! Now that we’ve extended our context with a term we need to somehow be able to tell Twelf the height of that term. This smacks of the slightly fishy type of nbinds/lam: it’s meaning is that F x has the height N for *any* term x. This seems a little odd, why doesn’t the height of a functions body depend on its argument? We really ought to be specifying that whatever this x is, we know its height is z. This makes our new code

Now we specify that the height of x is zero. This means we have to change our block to

%block nbinds_block : block {x : term}{_ : nbinds x z}.With this modification else everything goes through unmodified. For fun, we can ask Twelf to actually compute some toy examples.

%solve deriv : nbinds (lam ([x] (lam [y] x))) N.This gives back that deriv : nbinds (lam ([x] lam ([y] x))) (s (s z)) as we’d hope. It’s always fun to run our proofs.

ConclusionHopefully that clears up some of the mystery of worlds in Twelf. Happily this doesn’t come up for a lot of simple uses of Twelf. As far as I know the entire constructive logic course at CMU sidesteps the issue with a quick “Stick %worlds () (...) before each totality check”.

It is completely invaluable if you’re doing anything under binders which turns out to be necessary for most interesting proofs about languages with binders. If nothing else, the more you know..

Those who enjoyed this post might profit from Dan Licata and Bob Harper’s paper on mechanizing metatheory.

Cheers,

<script type="text/javascript"> var disqus_shortname = 'codeco'; (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### Philip Wadler: An Open Letter to John Swinney

Dear John Swinney,

I sat in the gallery yesterday to watch the debate on Privacy and the State. As a member of the Open Rights Group, I have a keen interest in the subject.

The Identity Management and Privacy Principles, published in October 2014 with your name on the foreword, states in Section 4.6:

If a public service organisation needs to link personal information from different systems and databases (internally or between organisations), it should avoid sharing persistent identifiers; other mechanisms, such as matching, should be considered.Willie Rennie and Patrick Harvie drew attention to the proposal that stakeholders should share the Unique Citizen Reference Number (UCRN). Using the UCRN as a key would link multiple databases, in effect forming a super-database, which is what concerns those who object to the plan. In your closing speech, Harvie intervened to ask you to acknowledge that the proposal breaches the Scottish Government's own guidelines. You responded:

I do not believe that the proposal breaches the data privacy principles that we set out.Time was short, so you said no more, but I invite you now to elaborate on your bald denial. The proposal certainly appears to contravene the principle advocated by your own document---how can you claim it does not?

It is not only your own guidelines which question your plan. The British Medical Association and the Royal College of General Practitioners have raised concerns about sharing information collected by the NHS with HMRC, and the UK Information Commissioner has warned that the proposal may breach European and British data protection laws. Both these criticism were raised during the debate, but ignored by you---I invite you to answer them as well.

There are ways forward that meet the needs of government and citizens that are far less problematic. I welcome your offer to review the proposals, and I hope that in light of these criticisms the Scottish Government will rethink its plans.

Yours,

Philip Wadler

Professor of Theoretical Computer Science

School of Informatics

University of Edinburgh

Related:

Minutes of the debate on Privacy and the State

Identity Management and Privacy Principles

Report of the debate from BBC News