• en

OCaml Planet

The OCaml Planet aggregates various blogs from the OCaml community. If you would like to be added, read the Planet syndication HOWTO.

Weekly News — Caml Weekly News, Nov 25, 2014

  1. Cmdliner 0.9.6
  2. Go Oracle like facility for Ocaml?
  3. Call for Presentations: Compose Conference [New York, Jan 30-Feb 1]
  4. Other OCaml News

2-or-more approximation for intuitionistic logic — GaGallium, Nov 25, 2014

I just finished the proof of a property of the simply-typed lambda-calculus that hopefully can serve as a termination argument to decide whether a type has a unique inhabitant.

http://gallium.inria.fr/~scherer/drafts/2-or-more-approximation.pdf

The 10-pages note containing the proof is available, and all comments are warmly welcome -- in particular about an already-existing proof of this result, I don't know about any. The rest of this post is (a HeVeA rendering of) the introduction, motivatin…

Read more...

A HoTT PhD position in Ljubljana — Andrej Bauer, Nov 22, 2014

I am looking for a PhD student in mathematics. Full tuition & stipend will be provided for a period of three years, which is also the official length of the programme. The topic of research is somewhat flexible and varies from constructive models of homotopy type theory to development of a programming language for a proof assistant based on dependent type theory, see the short summary of the Effmath project for a more detailed description.

The candidate should have as many of the following d…

Read more...

Menhir — Yan Shvartzshnaider, Nov 20, 2014



This blog post about  -  Menhir.


According to Wikipedia:

A menhir (French, from Middle Breton: men, "stone" and hir, "long"[1]), standing stone, orthostat, or lith is a large upright standing stone.
Coincidently, Menhir, is also the name for LR(1) parser generator for OCaml.
 
I followed the recommendation in the Real World OCaml to use it, rather than ocamlyacc:
"Menhir is an alternative parser generator that is generally superior to the venerable ocamlyacc, which dates back quite a few…
Read more...

Cmdliner 0.9.6 — Daniel Bünzli, Nov 18, 2014

Release of Cmdliner 0.9.6, consult the release notes for details.

Weekly News — Caml Weekly News, Nov 18, 2014

  1. containers 0.5
  2. OCaml opportunities in London
  3. opam-query 1.0
  4. Go Oracle like facility for Ocaml?
  5. Other OCaml News

How to choose a teaching language — Jane Street, Nov 18, 2014

If you were teaching a programming course, what language would you teach it in?

I like this question because it has any number of good answers, each quite different from the other, and each emblematic of a different approach to what programming is about.

The first formal programming class I took was COS 217 at Princeton, taught by the excellent (and at the time, I thought, terrifying) Anne Rogers. The course was (and is) taught in C, and the intellectual approach of the class was to start from t…

Read more...

ocamldebug — Mads Hartman, Nov 15, 2014

When I first read about the time-travel feature of the ocaml debugger I was very intrigued but never got around to trying it out in practice at work. This weekend I decided to give it a go.

I wanted to try it out on a simple but non-trivial program (in terms of setup, i.e. a program that requires opam packages to compile) so I used the hello world example of the ocaml-cohttp library.

1 Configuration

Before the ocamldebugger can work with your programs they need to be compiled with the -…

Read more...

The Magic of Thunk - Async — Xinuo Chen, Nov 13, 2014

async

Currently in post-production

The Magic of Thunk - Lazy — Xinuo Chen, Nov 13, 2014

lazy

The dark side of thunk

As discussed previously, thunk is used to encapsulate computations for later uses. Although we may not evaluate a thunk yet, we know its value is determined. However, it has a weakness: when we invoke a thunk repeatedly, the same computation inside it gets carried out again and again, despite of the fact that the results returned are always identical. For example,

let fibonacci n =  
  let rec fib a b i =
    if i = n then a
    else fib b (a+b) (i+1)
  in 
  fib 0 1 0…
Read more...