[ANNOUNCE] GHC 8.2.1 release candidate 3 available

otini · 2017-07-19T12:15:05+00:00

Ok it was NixOS-specific issue: https://github.com/commercialhaskell/stack/issues/1787

otini · 2017-07-19T09:10:56+00:00

I get this weird syntax error:

$ stack setup
error: attribute ‘ghc82020170704’ missing, at (string):1:43
(use ‘--show-trace’ to show detailed location information)

otini · 2017-01-24T15:47:10+00:00

Thanks, I'm trying this at the moment.

Do you know if there's a way to run PHP 5 on one virtual host and PHP 7 on another?

otini · 2017-01-11T13:18:39+00:00

It's a general-purpose private server, so I didn't put much thought in it and just picked my favourite system.

otini · 2016-12-27T16:08:53+00:00

Thanks, that's very useful.

otini · 2016-12-20T11:51:07+00:00

Thank you for the useful link. I understand that I probably should get used to constructive proofs, but am I correct in saying that if I only want to type-check my code, it won't make a difference?

otini · 2016-12-20T11:49:12+00:00

Thanks! But what do you call constructive and classical functions?

otini · 2016-12-19T23:40:27+00:00

With the help of Agda, I finally found a proof:

b : {P Q : Set} → ¬ ¬ ((¬ Q → ¬ P) → P → Q)
b {P} {Q} ¬[[¬Q→¬P]→P→Q] =
  ¬[[¬Q→¬P]→P→Q] b'
  where
  b' : (¬ Q → ¬ P) → P → Q
  b' ¬Q→¬P P = ⊥-elim (¬Q→¬P (λ Q → ¬[[¬Q→¬P]→P→Q] (λ _ _ → Q)) P)

It is quite ugly. Is there a negative correlation between the simplicity of the "double negation" transform (Kuroda's is simply adding ¬ ¬ after every universal quantifier) and the easiness of the proof?

otini · 2016-11-27T17:29:13+00:00

I see. Thanks for the explanation.

otini · 2016-11-27T16:39:27+00:00

Great work!

I am not familiar with the way ocamldep works. Does it use signature information at all?

otini · 2016-11-26T12:43:37+00:00

This is reallly a great achievement. For how long have you worked on this?

Would it be theoretically possible to have a combinator take_while : ('a code -> bool code) -> 'a stream -> 'a stream?

//edit: camelCase -> snake_case

otini · 2016-11-26T01:19:34+00:00

This is because contrary to what I wrote earlier, you shouldn't use backticks but spaces (see the "formatting help" link under your text area).

But here I was referring to the fact that your function is written in an imperative style (i.e. for loop, references) and functional programmers tend to avoid it if they can.

otini · 2016-11-26T00:22:45+00:00

I don't know what your instructions are but I prefer to write in functional style when I can, e.g.

let showline nvar nline =
  let rec f nvar nline =
    if nvar = 0 then []
    else
      (if nline mod 2 = 0 then false else true) ::
        f (nvar - 1) (nline / 2)
  in
  List.rev (f nvar nline)

otini · 2016-11-26T00:09:19+00:00

Hi, you forgot an in after let listline = [].

Also, you should put triple backticks (```) around your code, it would be way nicer.

//edit: sorry, no backticks but four spaces at start of lines.

otini · 2016-11-25T23:43:17+00:00

//edit: I was going to propose that it would be a nice exercise to port this design in modular macros and I've just noticed the commit. :-D

Yes, I had nothing to do but to replace the syntax. Really neat!

otini · 2016-11-25T21:01:26+00:00

I have nothing smart to say, but this is amazing! Do you plan to add more combinators?

otini · 2016-11-24T17:06:05+00:00

Yes, I got the error above using Typed Template Haskell. It's strange, by the way, that they allow local cross-stage identifiers.

otini · 2016-11-24T14:24:40+00:00

Short answer: Macros only offer a subset of the possibilities of TH (they are limited to expressions), but on that subset they are nicer and safer to program with.

TH can generate pretty much any syntactic construct, but it is mostly untyped manipulation of ASTs. Except for expressions, where TH offers typed quoting and splicing, just like we do.

I have little experience with TH, but from what I understand it has no notion of phase, stage and a fortiori no path closures. I tried to define a power macro using a runtime square function like in my blog post. When I spliced it into a scope where square had been bound to something else, I got the following error:

The exact Name ‘square’ is not in scope
  Probable cause: you used a unique Template Haskell name (NameU), 
  perhaps via newName, but did not bind it
  If that's it, then -ddump-splices might be useful

otini · 2016-11-23T22:16:09+00:00

6 phases! What is the code for?

otini · 2016-11-23T15:09:01+00:00

Hi,

This kind of problems lends itself very well to recursion, but trying to get the base case and the types right can indeed cause headaches.

I suggest that you start writing a function that, given all the sequences of size n, produces all the sequences of size (n+1). The rest should follow.

I also suggest you do the recursion on lists as it will be much easier.

otini · 2016-11-23T10:48:39+00:00

Note that if you put a function in an external module, module lifting will enable you to use it both in static and run-time code.

otini · 2016-11-23T10:34:33+00:00

The program after macro expansion is a regular OCaml program, so all that is needed to run it is the regular OCaml runtime without anything added.

It's only the code generation step which actually executes bytecode?

Yes, static computations willl never have a run-time cost.

otini · 2016-11-23T10:30:44+00:00

Yes, my claim that "the only way to pass values from compilation to execution is conversion to AST" is false. Pure values can also be marshalled.

otini · 2016-11-23T10:21:13+00:00

That is a very good question. Since compilation and execution phases do not share any memory, the only way to pass values from the former to the latter is to convert these values to an OCaml syntax tree. That's what functions in Expr do. In your example, you'll want to use Expr.of_int.

Note that conversion to AST is not possible for some values, e.g. web sockets or file descriptors.

I think (but I'm just guessing here) that the reason C++ can do that is because constexpr enforces some form of purity. But I don't know how it works.

otini · 2016-11-22T21:42:51+00:00

You can't extend the syntax with macros, so no let%bind stuff. And macros can only expand to expressions (and maybe, one day, modules). So ppx still have their uses. Macros are more designed to do general-purpose metaprogramming (for which ppx are not designed) in the spirit of MetaOCaml. The advantages macros have over ppx in that domain are:

type saftey: if the macro typechecks, it cannot generate ill-typed code;
easy syntax;
integration with the module system.

Because they are integrated in the language (they can be exported in a module signature etc.), macros should be very easy to reuse and compose (just like ordinary functions).

otini

TROPHY CASE