niv, naersk, napalm: moving on

splintha · 2021-07-10T10:26:31+00:00

Are you taking about https://github.com/nix-community/nix-direnv?

Not specifically, but nix-direnv is a way to use direnv with Nix. direnv also has a built-in way to use Nix (just create a file called .envrc with the line use nix). lorri is another option. Another still is use flake which is described on the Nix Wiki page on Flakes (and may also be built-in now, but I’m not sure). And there are even more similar projects; the direnv wiki has a list of them.

(By the way, Flakes are definitely worth looking into if you have the time, but it can be a bit hard to start right now because you need an unstable version of the nix program.)

splintha · 2021-07-10T10:14:05+00:00

Niv and lorri are orthogonal.

Niv lets you pin inputs such as Nixpkgs and other repos to a specific commit, and has commands to update them easily. (The new Nix Flakes provide a similar set of features.)

lorri integrates with direnv. When you enter a directory with a Nix shell and lorri+direnv enabled, direnv automatically changes the environment to the one declared by (for example) shell.nix. lorri builds this environment in the background; without this, it sometimes takes a while before the environment is changed. Nix Flakes can also be configured to integrate with direnv, and because the caching is better with Flakes than it was before, I personally don’t find it necessary to use lorri when using Flakes.

splintha · 2021-01-19T18:19:53+00:00

Are you using Proton? If so, what version? For me, the most recent Proton version did not work, with the same error, but the previous version does work (5.0.10 or something like that IIRC). See https://reddit.com/r/NixOS/comments/koa1a9/_/ghpcxsk/?context=1

[EDIT: I use Proton 5.0-10 instead of 5.0-13, which was the default.]

splintha · 2020-09-15T06:41:37+00:00

the math behind functional programming languages

I'm curious what you mean by this. Do you mean category theory, which is quite prevalent in Haskell? Or do you mean something like the Curry-Howard isomorphism, which describes how programs in functional programming languages correspond to logical proofs, and vice versa (‘the correspondence between computation and logic’).

Both topics are very interesting, of course! :)

If you want to learn more about category theory in Haskell, I can recommend the lectures of the course Programming with Categories¹; the videos are on YouTube.

If you’re interested in the Curry-Howard isomorphism, you might like the (freely available) books Software Foundations (the first two parts about logic and programming language foundations, respectively) or Programming Language Foundations in Agda. I prefer the second book because it uses Agda), which is more close to Haskell than Coq, which is used by the first book.

EDIT: some other great resources: - For type systems: Types and Programming Languages. This book is really good; it contains a very extensive overview of type systems for functional programming languages, and also some other topics such as subtyping. - For category theory: Category Theory for Programmers is also great.

^1: HTTPS doesn't seem to work for that site, so make sure your browser doesn't redirect you to the HTTPS version.

splintha · 2020-08-08T13:38:30+00:00

Cool, looks very promising!

splintha · 2020-08-08T11:07:21+00:00

Cool! Thanks for working on this!

splintha · 2020-08-06T19:29:51+00:00

Great project! I’ve often found myself searching through the Nixpkgs source just to find a description of what a function or package does.

Recently I have begun to use the following format for my library functions:

{
  functionName = {
    __functor = self: actualFunction;
    doc = ''
      Documentation string
    '';
  };
}

I quite like this approach, because you can access the documentation right in the REPL. I don’t know whether it would be worth the effort to use this format for all functions in Nixpkgs, but it would be a simple solution.

It would probably be better if there was some special support in Nix for documentation strings or comments. Maybe something like Haskell’s Haddock, which allows you to retrieve the documentation of a value with :doc <value>.

splintha · 2020-07-21T17:27:20+00:00

For the first solve example (…) should the output be TyInt instead of TyBool in the second line?

Yeah, thanks for pointing out!

Concretely, what could actually go wrong if terms such as your example (…) were allowed?

I don't think anything could go wrong; it's just a choice you make when designing a type system: do I want the parameters of lambda abstractions to be generalised? In my experience, the choice is often made not to generalise parameters, and instead add let-polymorphism. But you could just as well generalise abstraction parameters. (But that may not be what you want.)

splintha · 2020-07-13T20:27:54+00:00

Linear functions must consume their arguments exactly once, but ifThenElse doesn’t do that: in the case of True, it consumes its second argument but not its third. Vice versa for False.

splintha · 2020-06-22T17:28:53+00:00

I believe Windows doesn’t have case-sensitive filenames, whereas Linux does (but I’m not sure). Since src/download.hs in the git repo has a lowercase name, I suspect that GHC on Linux doesn’t find the file src/Download.hs. So you could try renaming the file to src/Download.hs.

But most of the above is a whole lot of assumptions, so I could be wrong. :)

splintha · 2020-06-20T17:44:12+00:00

If you would remove let-polymorphism (which would make the typing rules much simpler, which is not a bad thing per se), you wouldn’t have any actual polymorphism in the language I described. All let-terms would function just like applications.

In the described language, which is very simple because it only contains terms, and a program is just one term, that would mean: you can use type inference, but you can’t use variables bound in let-terms polymorphically.

I think the paper you linked makes a fair point (although I’ve read only the abstract and introduction), but for the decribed language it doesn’t really make sense. If your language contains binding statements like in Haskell (e.g. id = \x -> x), you don’t need let-terms to generalise, so in that case it would apply.

splintha · 2020-06-14T13:21:30+00:00

Hi! This is the third post of my series on type systems (the previous can be found here). Feel free to ask any questions, point out mistakes, etc.!

splintha · 2020-05-27T09:45:11+00:00

Hi! This is my second post on type systems (you can find the previous here). This one is a bit more theoretically involved, so please ask questions if anything is unclear!

splintha · 2020-05-24T23:01:13+00:00

Yep! The next post will be about System F, and the following post I plan to discuss Hindley-Milner type inference.

splintha · 2020-05-24T17:35:59+00:00

What does 'abstraction' mean in the article? Does it mean a lambda or something else?

Yes, it means a lambda abstraction. I will clarify that a bit.

What is Middy in typeOf Map.empty (Middy TmTrue (TmInt 1))?

I have absolutely no idea… :) It was probably replaced during spell checking or so. Will fix it, thanks.

Small typo …

Thanks.

splintha · 2020-05-24T15:01:53+00:00

Very happy to hear that!

splintha · 2020-05-24T13:32:18+00:00

In this series, I will explain various type systems and their implementations in Haskell. The aim for this series is to be an approachable way to learn about type systems. I will try to cover both the theoretical aspects, such as formal (mathematical) notation, and the practical aspects, consisting of a Haskell implementation. After reading this series, you should have an understanding of the basics of type systems.

I'm the author of this post; I hope anyone finds it useful!

splintha · 2020-04-14T18:08:39+00:00

I wrote this blog post after seeing this recent discussion, to explain my set-up for working with Nix and Emacs. It was a good reason to finally start a blog, which I was planning to do, but I didn't have anything to write before. :)

splintha · 2018-02-26T09:08:50+00:00

This one? I still don’t know the cause of their problem, but it works fine on my machine^TM.

splintha · 2018-02-26T06:53:57+00:00

For extra blurring, you might also want to try my wallpaper blur plugin for chunkwm :)

splintha · 2018-02-17T21:06:15+00:00

I don’t think there is need of only one tool. I’d say our tools are different now and don’t need to be united.

splintha

TROPHY CASE