Forem: domagoj miskovic

Flake My Life 3 - a snowstorm of errors!

domagoj miskovic — Thu, 20 Apr 2023 11:47:30 +0000

In my last post, I discussed mapping functions from the builtins and lib in the minimal template flake.nix. Now, let's finish configuring NixOS as a flake.

Initializing the directory with git

I initialized the directory using git init nix-config and loaded it into Vscode. After making necessary changes to flake.nix, I copied extra configuration parts from my configuration.nix. I won't modify home.nix for now and will keep the programs declared in configuration.nix.

Resolving git issues

I messed up something while uploading the directory to git through Vscode, so I deleted the .git directory and tried initializing it again. Not the elegant solution yeah.

I found a helpful tutorial by Tweag on understanding Git concepts here. After committing my changes and creating a repository on GitHub, I tried to apply the flake configuration without uploading the directory, but it didn't work.

Debugging flake rebuild failure

I got an error when running sudo nixos-rebuild switch --flake .#nixos. I tried changing the input section of my flake.nix to reference nixos-unstable and even removed the unstable option, but still faced errors.

❯ sudo nixos-rebuild switch --flake .#nixos
warning: updating lock file '/home/stablejoy/nix-config/flake.lock':
• Updated input 'nixpkgs':
    'github:nixos/nixpkgs/0cf4274b5d06325bd16dbf879a30981bc283e58a' (2023-02-19)
  → 'github:nixos/nixpkgs/bb2009ca185d97813e75736c2b8d1d8bb81bde05' (2023-04-19)
warning: Git tree '/home/stablejoy/nix-config' is dirty
error: attribute 'nixpkgs.config.allowUnfree' already defined at /nix/store/8ji8d4jrs8w8p59x39j3krq3kmay8h85-source/nixos/configuration.nix:34:7

at /nix/store/8ji8d4jrs8w8p59x39j3krq3kmay8h85-source/nixos/configuration.nix:137:3:

          136|   # Allow unfree packages
          137|   nixpkgs.config.allowUnfree = true;
             |   ^
          138|
(use '--show-trace' to show detailed location information)

OK, so I removed the double entry and tried again the flake build command and.. it works! But something looks odd. Why is it downloading so much? I thought a flake kind of transforms the system into a flake. What is happening? I guess since I haven't updated my NixOS system in more than couple days already it is downloading the new versions of dependencies and packages.

After 14 minutes I get this output:

nix-config on  master 
❯ sudo nixos-rebuild switch --flake .#nixos
[sudo] password for stablejoy: 
building the system configuration...
...
activating the configuration...
setting up /etc...
restarting systemd...
...
the following new units were started: NetworkManager-dispatcher.service, run-credentials-systemd\x2dvconsole\x2dsetup.service.mount, systemd-hostnamed.service, systemd-vconsole-setup.service

nix-config on  master took 14m46s

Is this it? I copy paste the output to GPT4 wishing for someone to just say yes, you did it. You got yourself a flake.

Congratulations! It seems like your NixOS rebuild has succeeded this time. The output you provided shows that the system configuration was built, and various services were stopped, changed, restarted, or started as needed. Now that you have successfully applied the flake configuration, you can continue to make changes to your NixOS setup and rebuild as necessary.

So how do we now update the system? I don't think I can use the sudo nixos-rebulid switch command anymore.

What's next now that we have a flake?

So the flake.lock is a generated file that records the exact versions of the flake inputs, like nixpkgs. When we update our flake enabled NixOS we will use nix flake update which will update the flake.lock to the latest available versions of the flake inputs. So the process goes like:

nix flake update
sudo nixos-rebuild switch --flake .#hostname

Also, the #hostname should be changed to one's own hostname (as declared in configuration.nix) in case this looks confusing. Yes, Nix is declarative and functional so when I first saw this #hostname I was thinking this is could be like bultins.currentSystem which gets the current system version so maybe I don't have to write my own hostname, maybe the #hostname picks up the system hostname. But this isn't the case apparently.

Let's add the Neovim flake

I'd like to add this Neovim flake now to my flake-enabled NixOS. We can run the flake with nix run github:jordanisaacs/neovim-flake but it won't stay in the system so how do we do we add it permanently? We need to add the neovim flake to our inputs section in the flake.nix as it says in the TODO: part of the minimal flake.nix. Let's do that! Our inputs attribute set looks like this now:

inputs = {
    # Nixpkgs
    nixpkgs.url = "github:nixos/nixpkgs";  # Use unstable channel instead of release

    # Home manager
    home-manager.url = "github:nix-community/home-manager"; 
    home-manager.inputs.nixpkgs.follows = "nixpkgs"; 

    # TODO: Add any other flake you might need
    # hardware.url = "github:nixos/nixos-hardware"; 

    # Shameless plug: looking for a way to nixify your themes and make
    # everything match nicely? Try nix-colors!
    # nix-colors.url = "github:misterio77/nix-colors";
  };

Let's add the neovim flake under the hardware.url set:

# TODO: Add any other flake you might need
    # hardware.url = "github:nixos/nixos-hardware"; 

    neovim-flake = {
      url = "github:jordanisaacs/neovim-flake";
      inputs.nixpkgs.follows = "nixpkgs";
    }

Now I asked GPT what does the inputs.nixpkgs.follows = "nixpkgs"; mean in this context?

When you specify follows = "nixpkgs";, you tell the neovim-flake to use the same nixpkgs input as the one defined in your flake, rather than fetching its own version of nixpkgs. This can prevent potential issues that may arise if the neovim-flake were to use a different version of nixpkgs that is not compatible with the packages in your main flake.

OK, that makes sense. I add the set and then write the file in Vscode. Vscode is then showing 1 pending changes, then with the + sign in Vscode we stage the changes, and then commit the changes with a commit message: adding the neovim flake into flake.nix so that it can be used as a flake input and accept commit changes with that little check mark on the right, then sync changes with the big green button.

OK, let's try to update our flake and see if this will be enough to have neovim flake on our system:

nix-config on  master 
❯ sudo nixos-rebuild switch --flake .#nixos
building the system configuration...
stopping the following units: accounts-daemon.service
NOT restarting the following changed units: systemd-fsck@dev-disk-by\x2duuid-7A19\x2d66BE.service
activating the configuration...
setting up /etc...
reloading user units for stablejoy...
setting up tmpfiles
reloading the following units: dbus.service
restarting the following units: polkit.service
starting the following units: accounts-daemon.service

Great! It looks like it worked. If I try to run neovim or nvim will it work?

nix-config on  master took 33s 
❯ nvim
The program 'nvim' is not in your PATH. It is provided by several packages.
You can make it available in an ephemeral shell by typing one of the following:
  nix-shell -p neovim
  nix-shell -p neovim-unwrapped
  nix-shell -p vimPlugins.vim-elixir

Nope! Oh! I didn't add the neovim-flake to my outputs section of the flake.nix. But after adding it I get an error:

error: syntax error, unexpected ELLIPSIS, expecting '}'

       at /nix/store/1wri85b2fy8f0512pd4gg4dqx3mgjddb-source/flake.nix:25:51:

           24|
           25|   outputs = { nixpkgs, home-manager, neovim-flake ... }@inputs: {
             |                                                   ^
           26|     # NixOS configuration entrypoint

I forgot to add the comma , after the neovim-flake but it would be nice if the error message explained that.

Let's try again:

nix-config on  master took 2s 
❯ sudo nixos-rebuild switch --flake .#nixos
building the system configuration...
activating the configuration...
setting up /etc...
reloading user units for stablejoy...
setting up tmpfiles

nix-config on  master took 19s 
❯ nvim
The program 'nvim' is not in your PATH. It is provided by several packages.
...

Nope! So I ask GPT what's the problem and paste in the code and we get an answer:

In your flake.nix file, locate the part where you define your system configuration, and add neovim-flake.defaultPackage.${system} to the list of system packages.

Now why do we need to do that? Why do I need to edit two files instead of simply declaring the neovim-flake into the inputs. If we look at the outputs in the flake.nix we can see that the outputs picks up the configuration.nix from our system:

outputs = { nixpkgs, home-manager, neovim-flake, ... }@inputs: {
    # NixOS configuration entrypoint
    # Available through 'nixos-rebuild --flake .#your-hostname'
    nixosConfigurations = {
      # FIXME replace with your hostname
      nixos = nixpkgs.lib.nixosSystem {
        specialArgs = { inherit inputs; }; # Pass flake inputs to our config
        # > Our main nixos configuration file <
        modules = [ ./nixos/configuration.nix ];
      };
    };

Let's add the neovim-flake.defaultPackage.${system} into our configuration.nixlist of packages:

{ pkgs, ... }:

{
  environment.systemPackages = with pkgs; [
    # ...
    neovim-flake.defaultPackage.${pkgs.system}
  ];

  # ...
}

Nope! After trying to rebuild it we get again: error: undefined variable neovim-flake so GPT was kinda wrong about this. Let's investigate this issue again in the configuration.nix. Hmm I still don't understand why would I declare the neovim-flake into my configuration.nix when this line in flake.nix says specialArgs = { inherit inputs; }; # Pass flake inputs to our config so what's the issue here?

I forgot to update the flake

I completely forgot to do the nix flake update this whole time and only did the sudo nixos-rebuild switch --flake .#hostname. What happens now when I run both commands?

❯ nix flake update
warning: updating lock file '/home/stablejoy/nix-config/flake.lock':
• Updated input 'home-manager':
    'github:nix-community/home-manager/72ce74d3eae78a6b31538ea7ebe0c1fcf4a10f7a' (2023-02-20)
  → 'github:nix-community/home-manager/5160039edca28a7e66bad0cfc72a07c91d6768ad' (2023-04-20)
• Removed input 'home-manager/utils'
• Updated input 'nixpkgs':
    'github:nixos/nixpkgs/bb2009ca185d97813e75736c2b8d1d8bb81bde05' (2023-04-19)
  → 'github:nixos/nixpkgs/ba0027bc70ae3294250cb662516b6571c3f406c9' (2023-04-20)
[37.1 MiB DL]error: insufficient permission for adding an object to repository database .git/objects
fatal: cannot create an empty blob in the object database
error: program 'git' failed with exit code 128
(use '--show-trace' to show detailed location information)

Great! Another error! Do I have to use sudo with flakes? I thought not?

if you're updating a flake that is managed system-wide and owned by the root user (such as when using flakes for your NixOS system), you might need to use sudo to update the lock file.

After using the sudo with sudo nix flake update and trying the rebuild command now the system is fetching another gigabyte of packages. Why? It is fetching llvm and ark for example. Let's see what comes after this. The reason for this is probably that I forgot to even update the flake in the first place, I don't even remember now after all this error hunting. By watching the running output it seems it is rebuilding Plasma DE too and on top of that it is building something from source so it is taking some time now already.

OK, it's been over an hour or so and it is still building the whole source of Plasma DE, currently at 61% build phase. I'm now really confused. I have enabled flakes but somehow I still do not understand flakes. Why isn't this using a binary cache, why is it building from source? On top of that it is building firefox from source which is a nightmare. I have to think what to do next and read more about flakes. I think I will stop the compilation process because it is only making my system slow at the moment.

Flake My Life - setting up a minimal flake on NixOS

domagoj miskovic — Tue, 18 Apr 2023 14:33:51 +0000

These days I have been exploring lambda calculus through Nix language which will be the theme of another blog post. I've been trying out builtins commands with attribute sets, learning more about flakes, watching some great content on NixOS on YouTube, and playing with nix repl and nix-instantiate --eval. Overall, I think it's a great time to be learning Nix.

However, I haven't transformed my NixOS configuration into a flake yet. This time, I refuse to simply copy and paste an advanced configuration like I did when I started with NixOS.

The configs I managed to reproduce in the past were from:

utdemir/dotfile-nix - Utdemir was a great help when I ran into issues with reproducing the config. Our conversation on GitHub issue #29 was my first engagement on GitHub, and it was a such a positive and inspiring experience.

Your issue was really useful! Always good to know what's the pain points on a fresh install. To be honest, installing this repository from scratch likely won't be a click&forget experience, since I do not routinely test installing from scratch and using other machines other than mine. Let me know if I can help with anything (even if you're not using this repo).

gvolpe.com/blog/xmonad-polybar-nixos Reproducing this setup took me a couple of days, especially when dealing with the xmonad tiling window manager, which seemed very difficult to set up on NixOS.
Th0rgal/horus-nix-home This config was another great learning experience with a visually appealing theme. The setup was simple enough, requiring only a few tweaks to the sub-modules.

Going all over again, this time with a basic minimal setup.

Although I would love to use any of these three configurations again, I decided to take a more incremental approach. I wanted to find a minimal setup that I could build on with better understanding before attempting more advanced configurations. I discovered the NixOS-starter-config repository, which offers minimal and standard flake templates.

If this is your first trying flakes, or you're attempting to migrate your (simple) config to it; you should use the minimal version.

If you're here looking for inspiration/tips/good practices (and you already use flakes), or you're migrating a config that already has overlays and custom packages; try the standard version.

OK, let's try the minimal one for starters and then build on that. The goal is to transform an already installed basic NixOS system running the Plasma DE (so no complicated setups with tiling managers yet!) and then build on that.

We are first instructed to create a git directory (because flakes by default work with git):



cd ~/Documents # this can be anywhere basically
git init nix-config
cd nix-config

So now we have a flake.nix, a flake.lock, and two separate directories home-manager and nixos. So we can inspect now the files inside of these directories. I recommend not just simply copy pasting one's own configuration.nix or home.nix because the configuration.nix in the nixos folder is also a template. Yeah.. I see there are these overlays and overrides which I have no idea how they work. That's the next other thing I have to learn about. I do remember there is a NixCon 2019 or so, a talk by Graham about overrides and NixOS internals so that's for sure in the next 10 talks I plan to watch on Nix.



nix = {
    # This will add each flake input as a registry
    # To make nix3 commands consistent with your flake
    registry = lib.mapAttrs (_: value: { flake = value; }) inputs;

    # This will additionally add your inputs to the system's legacy channels
    # Making legacy nix commands consistent as well, awesome!
    nixPath = lib.mapAttrsToList (key: value: "${key}=${value.to.path}") config.nix.registry;

Now here we already face the first obstacle: I do not understand what this means. I read already couple times about this flakes registry. Is this only on my machine? Where is this registry? And what are the nix3 commands? Is this a typo? What is the number 3 next to the nix command?

I will ask GPT4 and copy paste this piece of code into it.

OK, so this piece of code defines two attributes: registry and nixPath. That's clear. How are these attributes defined and what do they actually do and what for?

registry: The purpose of the registry attribute is to create an attribute set that maps each input flake to a registry entry. A registry entry in Nix is a way to map a flake reference to a specific flake. In this case, we are creating a registry entry for each input flake with the same name as the input itself.

So what does this mean. After much talking with GPT it shows me that this registry is not some online package registry of flakes but a local registry simply defined with this piece of code in my configuration.nix. So I can input one or many flakes that will be pulled into the rebuild cycle. Now this does remind of sub-modules that we can import into a configuration.nix or a default.nix but this isn't the same. The flakes are referenced and not simply combined into one flake. Or they are in a way when defined in flake.nix?

The registry is a user-defined mapping of flake references to specific flakes, and it is not a global, system-wide resource like a package registry in other package managers.

To achieve this, the lib.mapAttrs function is used. lib.mapAttrs is a higher-order function that takes two arguments: a function and an attribute set. It applies the provided function to each key-value pair in the attribute set and returns a new attribute set with the same keys and the resulting values.

Now what and how does this function work? Just by reading this it looks like a general mapping function that maps an operation to a list of things transforming the first list into a new list, or to be precise in our case an attribute set.



registry = lib.mapAttrs (_: value: { flake = value; }) inputs;

Let's check the Nix reference manual at https://nixos.org/manual/nix/stable/language/builtins.html#builtins-mapAttrs to see the what this lib.mapAttrs does:

Apply function f to every element of attrset. As an example:



nix-repl> builtins.mapAttrs (name: value: value * 10) { a = 1; b = 2; }
{ a = 10; b = 20; }

So here we come to a higher-order mapping function which is the bread and butter of functional programming. Nix is a pure functional language based on lambda calculus so these concepts such as map, reduce, filter, and fold pop out often. This is the thing I love about Nix. It reminds me on Haskell which is dear to my heart but still conceptually difficult for me. Nix might be actually a nice step towards learning Haskell eventually and also Rust with its functional constructs. So let's simplify this a bit and maybe use a simpler map function with numbers and list of numbers to see how it works:

Let's create a function that would double its input. So if we give it a number 2 it will give us back a 4:



nix-repl> double = x: x * 2

nix-repl> double 2
4

Ok that seems easy enough. Now let's make a list of numbers:



nix-repl> numbers = [1 2 3 4 5 6]

nix-repl> numbers
[1 2 3 4 5 6]

Great! We have a doubling function and a list of numbers. Can we apply our double function to a list of numbers as same as we applied it to a single number?



nix-repl> double numbers
error: value is a list while an integer was expected

       at «string»:1:5:

            1|  x: x * 2
             |     ^

Nope. We can't. What do we do now? Now we come to the idea: How could we map the double function to each number of the list numbers? Or in other words, the map function takes two arguments: the function to be applied and the list of elements to which the function will be applied. Now is there a map function in Nix that we can use? Yes there is! And it's right above the mapAttrs function in the Nix reference manual at https://nixos.org/manual/nix/stable/language/builtins.html#builtins-map

So in Nix we have the map function that maps over lists and we have the mapAttrs function that maps over attribute sets.
So the solution is simple then:



nix-repl> map double numbers
[ 2 4 6 8 10 12 ]

# same could be done with a square function

nix-repl> square = x: x * x

nix-repl> map square numbers
[ 1 4 9 16 25 36 ]

But by observing this behavior we can tell that this will not work with attribute sets because attribute sets have keys and values which is also a kind of map so we are talking about different data structures. So our mapping function needs to be modified. Mindblowing right? All of this smells like a Functor but I won't deep dive into that right now.

Actually by studying the mapAttrs function on our double and numbers list will show the difference:



let
  lib = import <nixpkgs/lib>;
  doubleValue = _: value: value * 2;
  numbers = { one = 1; two = 2; three = 3; };
  doubledNumbers = lib.mapAttrs doubleValue numbers;
in
  doubledNumbers

We need to import the <nixpkgs/lib> because our simple map is built into nix while the mapAttrs is defined in the lib library which is a part of nixpkgs packages. Save that file as let's say mapAttrs.nix and then:



❯ nix-instantiate --eval mapAttrs.nix 
{ five = <CODE>; four = <CODE>; one = <CODE>; six = <CODE>; three = <CODE>; two = <CODE>; }

Wow! we can see it works! Yes, the <CODE> parts are not showing because Nix is a lazy language, it only evaluates what is needed or to put it in better terms:

Nix only evaluates the function for a specific key-value pair when the corresponding value is accessed in the resulting attribute set.

If we add --strict option to our evaluation then we can see the result and the attribute sets will be evaluated:



❯ nix-instantiate --eval --strict mapAttrs.nix 
{ five = 10; four = 8; one = 2; six = 12; three = 6; two = 4; }

Wonderful! But what else can we see from this? We can see that the objects in this resulting set are unordered. While lists in Nix are ordered collections of elements that preserve the order the attribute sets are unordered because they are designed to be accessed by their keys, rather than the order of the elements.

So what about our flake?

Let's leave our deep dive into mapping functions and look again our flake registry definition.



registry = lib.mapAttrs (_: value: { flake = value; }) inputs;

So the result of our function over the flake attribute set will be stored in the registry attribute set which is basically a variable called registry. Then it become pretty obvious by now what the lib.mapAttrs does - a function that transforms the key-value pairs, and an attribute set to apply the transformation on. But now we come to the second part of the definition which is a lambda function that takes two arguments, _: and values: Now the underscore is used in cases when the key is not used in the function body same as in our previous example when we doubled the attribute set with doubleValue = _: value: value * 2; In this case we are interested in the doubling of the value while the key is empty. This is a concept known in functional language but I still need to see more examples of it.

OK I have talked more with GPT and this quote actually brings things nicely in line:

When you apply lib.mapAttrs (_: value: { flake = value; }) inputs;, it will iterate over the key-value pairs in the inputs attribute set, and for each key-value pair, it will create a new attribute set with the attribute flake set to the original value. The resulting registry attribute set will have the same keys as the inputs attribute set, but the values will be wrapped in a new attribute set with the flake attribute.

So if our inputs attribute set looks like this:



{
  nixpkgs = ...;
  flake-utils = ...;
}

After applying the registry function it will look like this:



{
  nixpkgs = { flake = ...; };
  flake-utils = { flake = ...; };
}

This finally makes so much sense. Now I just need to reread all this exploration couple times, meditate on it, sleep over it, and then again try to install flakes. Flake my life, this isn't easy at all but is super interesting. I never had this much fun configuring the system. I am learning programming and configuring at the same time while on top of it all everything is functional and there are lambda functions everywhere. How amazing is that!

But wait did I setup my flake? No I didn't. But I learned a lot and I have been doing this for hours today whole day. So much from my simple flake setup. But I will flake myself soon! I need to rest and watch some Nix talk and then try out the flake bit again. Then post about it next time.

Flake my life - how do nix flakes work?

domagoj miskovic — Wed, 12 Apr 2023 12:29:55 +0000

So I’m watching the excellent video Jake Hamilton "NixOS Flake tour" because I don't really understand how flakes work. Conceptually it seems clear but there is strange deepness to it too. What are flakes? Are flakes a natural extension or progression of nix expressions? I'd like to setup my system with flakes but it all seems foggy and unclear.

I used to have my NixOS setup with a tiling manager and various configs I copied from other experienced NixOS users but all that was done with a configuration.nix and home-manager and cachix as well. And then there was this really nice xmonad setup by Gabriel Volpe I managed to reproduce and which is a flake too, but after analyzing it and studying all the modules I still haven't actually understand how flakes work. His setup is at github link. Then came the time when I didn't use NixOS and in the mean time flakes have taken over the world it seems. Now I have just the plain plasma DE and simply wish to setup a basic flake system with a home-manager and one output machine. But so far it seems I cannot understand how flakes actually work. I have just applied for Summer of Nix 2023 and although I am incredibly excited about it and wish to do my best if it happens for me, I am almost feeling depressed since I can't seem to understand even how flakes work. How will I jump into the ocean of Nix expressions then?

So Jake very quickly mentions the snowfall-lib he wrote, a project of his. What does that mean? Is the snowflake-lib a library or a program or just another nix expression that would somehow automate flake related stuff? Jake says it “kind of does the boring work of wiring things together” so I guess I will understand more soon. There is a reason he has the folders organized the way they are setup and maybe the snowfall-lib does that for him or the folders need to be setup like that in advance?

.. because those are conventions from snowfall-lib which let’s me just say hey here is my directory with all of my stuff in it and it will import everything and hook it all up. I’m actually using the slightly more complex method here. I could switch this out to snowfall lib.makeFlake but once upon a time I needed access to this lib here. So snowfall-lib, go check it out..

I have no idea what this means. But I'm sure it's just some context beyond my level of understanding for now. I'm still a NixOS newbie.

So I go now to snowfall-lib on snowfall homepage on github and here we see that snowflake is built on top of flake-utils-plus and that snowflake is described as Unified configuration for systems, packages, modules, shells, templates, and more with Nix Flakes.

Oh I see. It seems without this snowfall library two or more users creating different flakes might end up with creating different set of folders or directories in the flake directory. So this means although flakes are reproducible they themselves appear to be impure because of different sets of directories? This is only important for the snowfall library for now since the library can potentially process all the flakes and automate stuff only if the flakes would respect the standard way in which flake directories are created. But since there is no standard way flakes directories are created snowfall enforces that which in turn enables the library to do the automation work. This is so far how I understand how this works.

Oh, now I see he uses deploy-rs for deployment which means this is another tool for automating nix flows. So now conceptually we have snowflake-lib, which is built on top of flake-utils-plus that uses the deploy-rs tool for deployment of outputs? Is deploy-rs something like NixOps? Now why would we need a deployment tool? I guess I will read now the serokell blog post on their tool delpoy-rs:

But reading it I understand that I should go out of this rabbit hole and try to find something on flakes. And in the article the often mentioned article from Tweag is referenced which is at https://www.tweag.io/blog/2020-06-25-eval-cache/

In the past, you might use the NIX_PATH environment variable to allow your project to find Nixpkgs. In the world of flakes, this is no longer allowed: flakes have to declare their dependencies explicitly,
and these dependencies have to be locked to specific revisions.

So this makes sense actually. But now this brings us to cache invalidation which is a serious problem in computer science! The cache itself is not the problem but the stale cache data that is not needed anymore and the problem of updating the cache field. So while on one hand you could update it too much and create much latency you could update it rarely and thus create stale unused data which might bring other problems in the system. This does seem like a hard problem. And this is where apparently flakes come to rescue.

Flakes bring what is called hermetic evaluation into the game, hermetic meaning completely sealed of from external influences. I ask now chatgpt4 to explain me the concept of hermetic evaluation in terms of nix flakes and it does a good job of it.

Chatgpt explains:

Hermetic evaluation in terms of Nix Flakes has the following implications:

Explicit dependencies: Nix Flakes forces you to declare all dependencies explicitly, making it clear which external resources are required for the build or evaluation process. This helps ensure that the build process is self-contained and reproducible.
Content-addressed storage: Nix Flakes uses content-addressed storage, which means that the outputs of a build are identified by the hash of their content. This ensures that if the inputs to a build haven't changed, the output will remain the same, regardless of external factors.
Isolated build environments: Nix creates isolated build environments for each package, with precisely defined inputs and no access to external resources. This ensures that the build process is not influenced by factors outside of the declared dependencies.
Lock files: Nix Flakes automatically generates lock files that "pin" the exact versions of dependencies used in a project. This ensures that the build remains reproducible, even when the upstream dependencies change.
Composability: Nix Flakes enables you to easily compose different projects together, ensuring that the dependencies between them are well-defined and isolated. This helps maintain the hermetic nature of the evaluation process when combining different Nix-based projects.

Actually now my understanding is that flakes are a natural extension of the nix system. It's like nix itself built on top of nix. The very reproducible nature of nix enables something such as flakes to work. So it's not even a question of inventing flakes, it is a question of finding them, this new solution that solves reproducibility of entire nix package configurations that have an arbitrary number of inputs. So now a flake can have more information cached in a way which will result in a faster evaluation time.

Since the flake’s lock file contains content hashes of all dependencies, this is enough to efficiently and completely capture all files that might influence the evaluation result. (In the future, we’ll optimise this a bit more: for example, if the flake is a Git repository, we can simply use the Git revision as the cache name.

Yeah, so in part three of the series on Nix Flakes the theme is setting up individual NixOS configurations as flakes. One of the things I didn't first like about home-manager is that it was somehow separated from the NixOS configuration but then there was a possibility to include home-manager as a standalone NixOS module and include it in the configuration.nix so that when one runs nixos-rebuild switch it would update the home-manager tree as well. But now when thinking of the flake view on this it does show that let's say I run my setup in a month or so what will happen? My nixos-rebuild switch will pull out a different git revision of packages from the nixpkgs tree. Does that mean it will not work? No, on the contrary, it will work but those will be newer versions of my packages. So now we have two points in time which does make the situation impure. The benefit of flakes is that our system configuration is fully reproducible meaning the packages and the nixpkgs are pinned down to their respective versions at the time when flake.lock is created. At least this is how I understand it now.

As the article goes let's check our NixOS version right now:



❯ nixos-version --json | jq -r .nixpkgsRevision
The program 'jq' is not in your PATH. You can make it available in an
ephemeral shell by typing:
  nix-shell -p jq

~/.config 
❯ nix-shell -p jq
this path will be fetched (0.00 MiB download, 0.01 MiB unpacked):
  /nix/store/65kn5z9zx4vwpib1v4b2kvc8mbalyrvj-jq-1.6-dev
copying path '/nix/store/65kn5z9zx4vwpib1v4b2kvc8mbalyrvj-jq-1.6-dev' from 'https://cache.nixos.org'...

~/.config via ❄  impure (shell) 
❯ nixos-version --json | jq -r .nixpkgsRevision
d9f759f2ea8d265d974a6e1259bd510ac5844c5d

So there is a unique number but you apparently can't extract the configuration.nix or any other modules file from this number.

Oh wow, and now a really cool quote comes:

It’s worth noting that any NixOS system configuration already violates the monorepo assumption: your system’s configuration.nix is not part of the nixpkgs repository.

I have never thought about this but it does make perfect sense. If my configuration.nix is not in a common repo this means it is impure and harder to use!

So another quote nicely outlines what flakes solve:

Reproducibility: the entire system configuration (including everything it depends on) is captured by the flake and its lock file. So if two people check out the same Git revision of a flake and build it, they should get the same result.
Traceability: nixos-version prints the Git revision of the top-level configuration flake, not its nixpkgs input.
Composability: it’s easy to pull in packages and modules from other repositories as flake inputs.

OK so here we go. Now I already am on NixOS unstable, so I just need to enable the flake enabling option in my configuration.nix but here is where the first problem arises because I am not sure if this relates to a pure NixOS system or a system that has just the Nix package manager installed:



nix.extraOptions = ''
  experimental-features = nix-command flakes
'';

The thing is that the NixOS wiki on Flakes states a different nix setting for the configuration.nix:



{ pkgs, ... }: {
  nix.settings.experimental-features = [ "nix-command" "flakes" ];
}

But then I stumble on this recommendation on NixOS discourse:



nix = {
   package = pkgs.nixFlakes;
   extraOptions = lib.optionalString (config.nix.package == pkgs.nixFlakes)
     "experimental-features = nix-command flakes";
};

Now yesterday I watched also excellent three hour video on setting up NixOS at NixOS Setup Guide from which I did:



nix = {
  package = pkgs.nixFlakes;
  extraOptions = "experimental-features = nix-command flakes";
};

Now what is going on here and why are these expressions different and yet apparently doing the same thing. Now we come to nix programming! I asked chatgpt to explain me the differences between all these expressions and after some chatting back and forth it is evident now:

that the first expression which was shared on NixOS discourse is actually conditionally enabling experimental features only in the case of flakes
the last expression actually enables experimental features in whatever case so not just for flakes.

How is the first expression conditionally enabling flakes is the cool part! With the lib.optionalString which is a function provided by the nix library.

The syntax is like:



lib.optionalString condition stringValue

In the first expression:



extraOptions = lib.optionalString (config.nix.package == pkgs.nixFlakes)
     "experimental-features = nix-command flakes";

the value of extraOptions is conditionally set to "experimental-features = nix-command flakes" only if config.nix.package is equal to pkgs.nixFlakes. This means that the "experimental-features" option will be included only when the system is using the nixFlakes package.

Ok so after seeing more chatgpt examples of lib.optionalString utility I see that it's a really practical way to include flags into builds and configurations that might or might not happen depending on some conditions.

This flake my life will need to go on. My goal is to make the simplest possible flake of my system and make sort of a spectrum of possible ways how the flake can expand from a simple to more complex system. I often find out complex flake configurations with just enough nix expressions variations and that makes it a bit more difficult for me to understand. But I learned the cool lib.optionalString though which is awesome!

Recursive/Attribute Sets of Nix Expressions

domagoj miskovic — Sat, 08 Apr 2023 13:20:57 +0000

This is going to be a beginner oriented exploration about a fundamental data structure in Nix language - Attribute sets.

Attribute sets are a collection of key-value pairs where each unique key is associated with a value. These key-value pairs or as we sometimes call them maps are also called in a more general term associative arrays, or dictionaries in Python, hashmaps in Java, objects in Javascript and so on.

The Nix manual states that attribute set is a collection of name-value-pairs (called attributes) enclosed in curly brackets ({}). Names and values are separated by an equal sign (=). Each value is an arbitrary expression terminated by a semicolon (;). Attributes can appear in any order and an attribute name may appear only once.

So this means they are unordered which goes along with Nix being lazy evaluated language. But the reason they are unordered is because they do not represent sequences but mappings of key-value-pairs. This made me think of category theory and another one of brilliant Bartosz Milewski lectures where he compared a table with cached functions.

In Nix language there are basically two kinds of these attribute sets. There are these regular non-recursive attribute sets that cannot reference any attribute within and then there are the non-regular recursive attribute sets that can access any attribute which means they can construct complex configurations and interdependent relationships between attributes. OK what does that mean? Because It took me a while to really understand the difference.

So the thing about the recursive attribute set is that one can refer to any attribute within the set.

A very small example of this would be:

rec {
  a = 1;
  b = a + 2; # b refers to a, which is defined in the same attribute set
  c = b * 3; # c refers to b, which is defined in the same attribute set
}

So what this means is that when we are designing complex build processes we can self reference within the set and access different values. Like deriving a new attribute from an existing one:

rec {
  user = "alice";
  homeDirectory = "/home/${user}";
}

Now this makes me think how come I can't recognize when I look at my configuration.nix file which expressions are recursive and which are not by just looking at the syntax. What I mean is that my user is declared with a set but there is no mention of a recursive set or the rec keyword. Now chatgpt answers me on this:

You are correct that recursive attribute sets are typically declared using the rec keyword. However, in NixOS and your configuration.nix file, you might not always see rec being used explicitly. This is because the NixOS configuration is built using the NixOS module system, which automatically handles the creation of recursive attribute sets when needed.

Oh cool. Then it explains a bit how that process goes.

So again what is an attribute set basically? An attribute set is a collection of key-value pairs. Like a dictionary or a phone book we have a key and a value.

{
    key = "value";
}

But we can write any other value such as a number 42, a string of “hello”, a path to a file in a system, a boolean value of true or false, a uri value or an address of a web site to say it more plainly, a list of things such as fruits, or even what is really cool - a nested attribute set:

{
  intVal = 42;
  strVal = "hello";
  pathVal = /etc/nixos/configuration.nix;
  boolVal = true;
  uriVal = "https://example.com";
  listVal = [ "apple" "banana" "cherry" ];
  nestedAttrSet = { keyA = "valueA"; keyB = "valueB"; };
  functionVal = x: y: x * y;
}

So a nested attribute set in Nix refers to an attribute set that is used as a value within another attribute set. But what does that mean? I asked ChatGPT to quickly create a phonebook of three contacts and show nested attribute sets. Now the same applies when making packages. You have the names of the packages but then you have a different build options and even instructions or functions with these build options. So even though a phonebook example looks pretty clear, this is just a very small example of nested attribute sets.

{
  phonebook = {
    contact1 = {
      name = "Alice";
      phoneNumber = "555-1234";
      email = "alice@example.com";
      address = {
        street = "123 Main St";
        city = "Anytown";
        state = "CA";
        zip = "12345";
      };
    };
    contact2 = {
      name = "Bob";
      phoneNumber = "555-5678";
      email = "bob@example.com";
      address = {
        street = "456 Elm St";
        city = "Sometown";
        state = "NY";
        zip = "67890";
      };
    };
    contact3 = {
      name = "Charlie";
      phoneNumber = "555-9876";
      email = "charlie@example.com";
      address = {
        street = "789 Oak St";
        city = "Othertown";
        state = "TX";
        zip = "24680";
      };
    };
  };
}

Now what this makes me think is are all attribute sets one-dimensional or are there multi-dimensional attribute sets. In some ways recursive sets I guess mimic that behavior. But not really. Recursive sets being able to reference values within themselves during a temporal state doesn't make them multi-dimensional. This just proves I do not quite understand what would multi-dimensional configuration actually mean in this context.

But that's OK. I am enjoying this exploration of nix attribute sets. Need to explore attribute sets more and how they can be constructed. Also keeping my attention to attribute sets and slowly expanding from that seems helpful because I seem to retain more information between sessions and it is easier to get back to it even for ten minutes.

finding rest in devops

domagoj miskovic — Sat, 11 Mar 2023 10:52:28 +0000

Going into AWSome clouds

It all began with a question my partner asked me. She asked what is a cloud engineer and what is cloud? I paused for a moment and said the cloud is like the plumbing between people and apps. It makes data and apps available to us at great scale and you don't have to hold the server in your hands and build it yourself. But then the cloud isn’t just that. It's so much more. It’s about connections and how complex relations happen between services and which ones work best for which workloads. And how much work and care and passion there is between the users and machines. Something like that. I began thinking more and more about the cloud days after that. I felt that hacking vibe and a wish to get into it deeper or higher. The thing is once you start thinking about the cloud you start thinking globally like on a massive scale.

aws makes it all together

So yeah, like for example I have used ssh and keys and shells, and have ran scripts on my linux, installed virtual machines and played with archlinuxes and recently spent much time tinkering with NixOS. Or like I know about load balancers from reading the hackernews and how sites are cached around the world for better latency for the users. These things pop out all the time. But that's just theory for me and constant shifting of my attention from this or that. The thing about AWS is that it actually helps me in staying focused with my learning because all that seemingly random stuff I read about here and there or have engaged a bit on my individual machines now starts to make sense and is reflected into a global computing picture which is not static at all. AWS makes you hold everything you know and then learn some more by engaging with their services. These services show you how stuff connects actually. You can try stuff out, not just think about it.

AWS gives all the playground on massive scale

But the great thing that inspires to go deeper into it is that AWS actually helps with the education and practical tools. There are these aws certifications and training, that test your knowledge of the concepts and the language and give a sort of framework through which one can see, have a bird eye view of what and how these services connect and what are the best and worst practices. I do love gentle hand holding and just love the general idea of certifications and how amazon is actually showing care about education through those. I didn't think like that before sadly. I was proud of being a loner explorer thinking acomplishing certs is boring. I underestimated their educational value and how they can help in seeing a larger picture of processes.

I discover that I know more than I thought

OK so I planned to do the cloud practitioner certification and have began a course on youtube. Then I signed up for a AWS online conference event that happened on 9th March because I read they will be offering free 75% off price vouchers for the certificates. Great! I really liked the talks and by the end of the day I got the associate solutions architect badge for the 75% price. I asked on aws reddit and in short I was recommended to do that one instead of the cloud practitioner one because of my poweruser background. So while I am far away from actually knowing how aws works I realized my previous random linux knowledge and lots of reading and trying stuff out is actually helping me to understand aws concepts. Yes they have specific names for theis services like EC2 or S3 or DynamoDB but I did read about NoSQL databases before, and I am familiar with running virtual machines and setting different parameters. So now somehow all that random stuff I did is actually coming together in this aws journey. I can learn how it all works on massive scale and go slowly through it. Yeah, and I bought the Stephane Maarek udemy course on solutions architect so Im studying now with better focus.

Im pretty excited in finding the right inspiration to learn devops and cloud with aws. This was the first post of my journey into devops and aws that had more to do with inpiration than technical issues. Stay tuned. I cant wait to write more technical stuff about the cloud. Its so exciting.

P.s. These images of clouds in Croatia throughout the blog post were taken by me.

n-days of hacking - This is the best way to eat popcorn

domagoj miskovic — Thu, 14 Apr 2022 17:09:48 +0000

How I discovered Ippsec and online cybersecurity training platforms

I am blogging about my pentesting voyage because it helps me to learn better. It keeps my information scope in control. When one begins to immerse oneself into a field one tends to jump back and forth into various interesting rabbit holes. And hacking has many of those, all pretty and sweet. At the same time the art of hacking is also being able to see through many many of those holes and find the way in. There are so many details and areas so good repetitive practice and documenting thinking through builds motivation and most important inspiration

Let me introduce my self briefly and the methodology that I will use. I have been tinkering with my linux boxes (Archlinux btw, debians and lately NixOS mostly) for more than a decade. My first linux was Slackware. It seems like ancient history to me honestly. I don’t work in IT, I am a professional classical guitarist and educator, but always, since my youth have I have felt drawn to computers and linux. Lately, I have been learning Haskell and functional programming because it feels mind expanding, but I kinda gave that up being overwhelmed with functors and monads at the same time being a parent and having a regular job in a local music school. Not to say functional programming did not actually help me in so many ways, like when I see some code now the way I think about it has changed, type oriented thinking helps in seeing how things compose together. I say a regular job because I am not too happy with it. Its kind of a straight jacket. This year I have been learning about NixOS declarative linux distribution which is completely configured with nix expressions. There in a single source of truth, the configuration.nix file and you can roll back and forth from generation to generation, basically you can have many versions of the same program on the same system and nothing gets corrupted. I am no programmer and have not written any kind of program except the most basic ones. I often read and copy-paste too much and enjoy exploring various rabbit holes like category theory, taking a bite too big to swallow. I love reading things I don’t know about. I wonder if that is some kind of imposter syndrome reverse shell.

I am familiar with various infosec terminology though, in the sense that I do know what nmap does, what TCP/IP means. I even used to read phrack issues from time to time. I spent much time reading all kinds of posts, deep diving on hackernews and on and so on. After ten years sometimes I feel I don't know much, just a bunch of very wide lateral surface like knowledge. Not much has been put into actual deep practice. Since most of these things I don’t really use or practice variations upon a theme I tend to forget them after a while. I am aware I might sound like a complete mess but I feel I am a hacker at heart. I do care for user experience and imagine a world where interacting with computers is well, more interactive. I used to play armagetronad game very well but after noticing my cortisol levels reaching up and wide I stopped suddenly and never played any games after it. I was good at it. But I thought about a gamified learning experience often and Imagined how the future of work are virtual gamified platforms. This is where Hack the Box blew my mind with it’s gamified hacking platform, a place where one can so to say have the cake and eat it too, where one can learn by doing, where one can play and learn at the same time and be a part a kind and receptive community of hackers.

I recently finished watching the amazing Mr. Robot series on Netflix. Elliot can move through the networks and do all kinds of hacks which inspired me to think more about security and the actions of a user and read bits on security here and there. But there is something else too. A hacker is somehow flexible and creative and has a superior control over his digital senses. He can break in, he can modify all kinds of files, noticing the patterns and knowing how even a tiny change in the code might change the complete state of the system, and all that is visible in the real world too. He can write an exploit, a work of art whose sole purpose is to deliver a payload that will somehow bring the system to its knees. It is sci-fi at its purest.

I discovered HackTheBox platform and Ippsec walkthroughs. Ippsec is the famous HackTheBox player who also made many, almost 250 and counting, video explanations of the boxes he breached. He works now for HTB and continues to work on new boxes and doing all kinds of interesting work. I read about him and how many people even call him a legend. That is inspiring. I was instantly hooked and blown away into million bits as if Rinzler himself threw that disc at me. He seems like a really nice guy and you can sense his love and enthusiasm when he talks. He is humble too which is an amazing quality to experience when listening to an educator. It helps one progress faster and removes many mental afflictions that may appear along the way. Speaking as an educator myself, having someone like that helps immensely since he is not pulling you into his own afflictions but allowing you to grow as an artist, as a person. Actually seeing someone moving like that and talking back and forth about the possible attacks and defenses made all the difference for me too. Somehow the static images of hacking pages turned into a movie, and seeing this movie opened my eyes to the true beauty of hacking.

I actually did buy the famous book Hacking The Art of Exploitation back in 2011 but unfortunately I never read that book, it seemed too hard, too low level for me at that time, which is too bad since it looks like a great book. I needed my Ippsec. But have no regrets! HackTheBox is here to stay and there has never been better time to learn hacking! Isn’t that amazing!? Wait, how amazing is that!?

Seeing Ippsec kindled that flame again and realizing you could hack all kinds of real boxes on a private virtual network with other players seemed so super exciting and again, mind blowing. But it’s not just that. It is amazing to see how someone moves around the network. While before I would read much and like statically configure something on my system, a hacker actually moves around the network and computers like USS Discovery. That is the inspiration I guess I was missing. Yes watching Ippsec is inspiring to say the least. It motivates you to learn about buffer overflows and php filters. You realize the shell commands are like various senses of a user and editing the code files is like search and replace actions, as if teleporting your actions into the distance of the digital grid you automate them, invoke reverse shells that connect to you and oh so many other goodies.

Let's pop the corn!

ippsec popcorn

So first I just watch the Ippsec popcorn video couple times and write a couple of notes here and there, not too many since I first want to listen to the way Ippsec speaks and the flow of it. Stuff like the php script into png file conversion eludes me the first time but by the next time I understand the idea of adding the beginning magic bytes from another legitimate file to the script so that the linux file command recognizes the script as a normal file. Looks hard at first but then it does get much easier.

Now watching it for the third time I am carefully stopping after each phrase and googling everything Ippsec is saying. I do know what is nmap and php and png and what it means to get a reverse shell but of course I have no idea how to do all these things. I am like a hacker impostor, I can follow the conversation but I have no actual idea what is happening. I can only fake it, but that’s a beginning too.

ppsec begins connecting to the virtual network with tmux which is a terminal multiplexer. He fires it up with a command

tmux new -s HTB

Now this is a very nifty program and I am only briefly familiar with it from my xmonad days. In a tmux session you can open multiple terminal windows inside tmux, so in a way it is like a tiling window manager but just for the terminal window. Nice and important feature of tmux is that the session is persistent which means that if you do get disconnected from the server the program on the server will keep running. I still don’t know the full implication on this but let’s go on. There is also a new multiplexer called zellij written in Rust which is a modal multiplexer and visually it also seems really nice to try it out. Zellij shows the commands in the bottom pane which is more user friendly than the tmux way. So I install rustup and then zellij.

$ curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
$ cargo install zellij

Ippsec taks about the importance of being organized:

Very first thing to do is find a way to stay organized. I just created a folder called boxes and labeled the hostname of each box. This one is called popcorn

I have been first using emacs with org mode and then switched to notion.so (I am actually using notion right now to write this) which has a really nice mobile app too but now I am also looking at obsidian too which has this temporal mapping and visual network of things you learn. In any case making good notes is very important. It makes all the difference when one is learning. One is repeating what one learns, formulating it in a variety of ways, thus going deeper into what one learns. It is extremely important. The next thing after taking notes is actually writing write-ups, blogging and streaming about what one learns. This helps in connecting with the community, which then helps in building motivation and persistence. Again, really important to take notes. And the level of expertise is not important, even more so, I wish there are more noobs documenting in detail how they go through these things. There is much to learn from that. Again, user experience and how one learns. It will help more people to learn IT.

Ippsec begins the reconnaissance phase with a nmap scan with options:

-sV for version, -sC to run safe scripts against it, it may be redundant to run both of these but I always do it out of habit. I put -oA formats because I don’t know if? I want to use the grepable format, the regular format or the xml. It might as well give me all.

The first thing he does is he goes to the 10.10.10.6 in the browser and gets the standard Apache server page it works!. I have no idea what nmap can actually do. Ok, so nmap is something called a port scanner. A port scanner is usually used in the initial phase of reconnaissance. It enumerates or tells you information about the system or the networks you’re scanning. nmap is like the eyes through which you can see what is happening around you, what things or systems are doing on the network, what doors or ports are open or closed, how many there are, but also which kind of systems are running behind these doors. It seems it is easy to begin with nmap but there is a lot of depth to it too.

I take the note to myself to do the corresponding courses on nmap on HackTheBox and TryHackMe and skim through the freely available nmap book by its original coder Fyodor. Again, nmap seems like a huge time investment in itself but for now maybe let’s continue and learn just the basics.

So my very first step is I turn on my burp proxy and we are going to refresh this, and I am going to change this host to be the domain name of the server (Host: popcorn.htb) and I do this just because of something called virtual host routing. The server is going to look at this header that I sent and if it’s set up as virtual host routing it will read this and potentially service to a different location... Not the case here.

Ippsec is using the professional burp license and as I learn the community one which is free has some limitations. I am wondering if these limitations will get in the way when attacking a single box on hackthebox or these limitations are appearing when attacking web applications with potentially several domains across the network. What are the limitations when using it for just a single web application on the hackthebox network? And I google alternatives such as open source tool ZAP. ZAP seems like a similar program so I would like to try to learn the basics of ZAP too. Update: I found this really nice and on point video from John Hammond where he explains the basics of burp and setting the DVWA application using a docker container. It is a really nice down to earth video and one of the best. The other source would be hackersploit videos on burp on youtube.

Burpsuite Basics

So the next step is, I am going to run dirb against it, you can use wwwfuzz dirbuster, there are a lot of programs you can run. I just run dirb.

dirb http:10.10.10.6 -r -o tmp.dirb

-r is going to make it so it doesn’t go into recursive mode and -o saves it as output.

Now what is actually dirb and what does it do? DIRB is a Web Content Scanner. It looks for existing (and/or hidden) Web Objects. It basically works by launching a dictionary based attack against a web server and analyzing the responses. Now, Ippsec turned off the reverse search this time because it would attack each subfolder of every folder and so on and so on. That's recursion. So it would take much time. Apparently this was not needed in this case but I learned what an recursive attack means. This is something familiar from Haskell. The output of dirb shows different pages on the server.

We have a http://popcorn.htb/cgi-bin/ (CODE:403|SIZE:287) It may be useful, we may wanna dirb this to see if there is any cgi scripts. We have index, index.html, server-status, test is interesting. Let’s open up test, and we probably have to turn intercept off, and we get the php info page. This tells us a bunch of information about the server, most importantly it shows us where php scripts are cached so if we have a local file inclusion we may be able to chain some of the knowledge gained from this to give us code execution. So we’ll keep that in our pocket in case it’s useful. We also see a /torrent link so I click this and see what this is. We do have an application, a torrent-hoster. So my first step is I generally always, and I say generally because I didn’t do it here, but I run searchsploit against the app. searchsploit is going to search exploitdb but it’s all local so it goes really fast.

And we do see one remote upload exploit

I will have to finish the blogpost here for now and continue next time. I would like to blog more often than waiting for something to be finished. This took me couple of weeks and juggling between family obligations and work and hacking is hard. Next time I am going to continue commenting the popcorn and eventually popping it myself. In the mean time I am studying burp, then setting up my virtual lab with metasploitable2 and learning more about linux text processing tools. Being quick on the command line and learning to filter files taking into account permissions, users, wildcards and regex is something I need to work on. I have watched the next two boxes from Ippsec. One is October and that one seems hard for me to understand since I don’t know anything about buffer overflows. The Arctic seemed easier but it was a windows machine and Ippsec used metasploit. So there is much learning to come! I am happy and super excited about this. Until soon.

Tron popcorn

100 days of NixOS

domagoj miskovic — Tue, 25 Jan 2022 19:20:06 +0000

NixOS operating system is a GNU/Linux distribution based on the Nix Package manager. NixOS is a Linux distribution same as Ubuntu is a Linux distribution. A distribution itself is a customized collection of software and tools packaged together with the Linux kernel. The kernel itself acts as a layer between the user-space where processes or programs live and the hardware, memory, cpu, devices and network devices that programs need to access to do stuff and move bits and bytes around.

How does the Nix package manager work and what is so special about the Nix package manager? Why should one care about it? There is a lovely intro with nice pictures about Nix and it's ecosystem on https://nixos.org/explore.html

This first day of 100 days of code has a bit of story telling and then some installation details that will come a bit after. I will try to express some things I feel inspired about. I am a beginner and have very limited knowledge and experience of NixOS system except exploring it for less than a year with breaks. So this purely comes from my own experience and the love I feel for its design principles and the declarative approach.

NixOS system together with the Nix package manager and the Nix programming language is a provisioning kind of operating environment. What does this really mean? Essentially, to put it simply, you are not supposed to actually do anything. You are supposed to define your actions using a lazy functional domain specific language called Nix to do the stuff for you. You write the wishes and instructions as functional code declarations or recipes and then the system does what you ask it to do. Now, the real difference lies in the fact that you are not simply writing down the commands, automating the steps that you would have to do by hand like in other distros or even on Windows. With Nix you are writing what and not how. You are actually using a functional language to express the way packages are built, the way your entire system will be. How cool is that?

Yes, there are package managers like Ubuntu’s apt-get and apt through which we install software by directly interacting with the manager, executing commands in real time such as sudo apt install some-program and sudo apt remove that program. But what actually happens when something goes wrong? How do you go back? What happens when your version of program does not play well with the rest of the system? What happens when something breaks and you wish you go back? What happens when you simply would like to try out something within a container like environment? With other package managers I am manually entering the commands. Even with an Ansible like playbook I would still have to write apt install. I would still have to write the how.

With Nix you are defining the system and the system then takes care of the commands and the how.

For example, how do you declare a new user into the system? What is a user in this case?

A User is a human being who operates a computer in the real world. If a user writes and compiles a computer program, the program, inhabiting the micro-civilization in the computer world, often looks exactly like his or her user counterpart in the real world, though exceptions exist for data pushers and programs written by multiple users. Users normally communicate with their programs by speaking or typing commands into their computers; on the other side of the screen, programs receive these impulses as "calls" which summon them to I/O towers to trade information with the other world. Many programs regard their users, both those who write programs and those who simply use them, as akin to gods, while others have been known to reject, deny, or attempt to manipulate them.

# Define a user account. Don't forget to set a password with ‘passwd’.
  users.users.dom = {
    createHome = true;
    isNormalUser = true;
    extraGroups = [ "wheel" "video" "audio" "disk" "networkmanager" ]; # Enable ‘sudo’ for the user.
    group = "users";
    home = "/home/dom";
    initialPassword = "nixos";
  };

And here we have a user:

Ok I love Tron and I fight for the users. Now,
this user declaration is from the configuration.nix file that defines my current freshly installed NixOS system. It is a simple bare bones configuration file written in a text editor. The beauty is I can write it all there, all the apps, services, the users, the settings, and so on, and the nixos will rebuild the system with these specifications. I just want to boot into a usable system and then work from there.

There are many complex nix configuration setups and some of those are simply amazing, integrating git actions, binary caches, home manager, but I wanted this time go from the vanilla beginning again.

So in any other Linux system you might add a user with:

# useradd -m -G additional_groups -s login_shell username

Yes, in Ubuntu maybe that is not needed, maybe you could click something and click your way through and setup another user. In Windows it is similar. There are some graphical interfaces from where you create a user. But with nix you simply declare it in a file as code, and then the system creates the user for you.

There is no work to be done except thinking about it and writing it down. You are also not learning or going through a variety of ways of how one can create, what one needs to click and so on, no, you are simply declaring what you want. This is very profound. There are much more complex examples like setting a database server with a user and installing for example python too. But again, one is declaring that without writing commands like install this. This is simply profound. This code can then be shared and reproduced with other users without worrying of the current state of other systems.

Here I begin again the 100 days of NixOS challenge. My previous attempt was at https://hackernoon.com/100-days-of-code-death-of-summer-on-the-island-of-nixos-gd1a3ws8 and also I documented some of my explorations on my github page at https://dooygoy.github.io/nixos-zoo/

Then I became a parent a year and a half ago and so after a while my laptop ended up with a windows 10 installed instead. The background is that I am not an IT professional, or as Big Pun would maybe have said it, I am not a player, I just love IT a lot.

Learning about parenting was hard at times, so I have stopped exploring Haskell and categories, and NixOS too after being with it for less than a year, but I came back just now. What changed? Well I learned as a parent that it is OK to learn in small bits, to find time when there is some, and keep learning without stressing how there is not much time.

NixOS ecosystem is a huge time investment but no worry, it is worth it, and while learning it, it might just happen that some other things become more clear and less confusing. The same thing happens with Haskell and learning about category theory. Although I ended up not actually implementing anything in Haskell, and most of my time I just wrote simple bits of code and tried to visualize functional structures, recently when I read some python code it made much sense to me, it seemed simple if I may say. Generally, learning functional programming helps in thinking about processes in a relaxed, space-like abstract level. You are not so concerned with the implementation but the meaning of it all, and what are the things that make the problem at hand. Something similar happens with NixOS. NixOS does seem hard and has a steep learning curve, but it also has a huge payoff in terms of understanding what is actually happening with the system. With Archlinux I was involved with the configuration of the system but it seemed more manual to me at times. I didn't automate anything back then but the NixOS invitation seemed much more appealing, something struck me the first time I glimpsed into the depths of the Nix ocean. Instant rollbacks to any previous time generation, rolling a virtual machine in an instant and bunch of other things I do not even understand yet.

Once you taste the fully declarative approach of the Nix package manager that makes the NixOS, it comes to your mind from time to time this provisional idea, and then it erases all your darling distributions and operating systems that you interacted with before. It comes to your mind when you download a phone app, or need to reinstall a package, or need to wait for a windows update that tries to talk you too. Suddenly, with NixOS, it is all there in the open, all expressed as nix expressions.

Well, what I really mean to say is that NixOS is something you secretly longed for if you ever spent time tinkering with archlinuxes and windowses of the world, but you still don’t know it. There is this feeling once you get the subtle idea of NixOS you realize, oh my, I can’t go back after this. I would only fool myself.

And now I stop the romantic ouverture and begin with the concrete steps I made during the installation.

Since I am on Windows 10 I use the program called Rufus to create a USB bootable stick with NixOS 21.11 GNOME edition. I burn it in dd mode.
I disable secure boot option in BIOS setup since this is still not fully resolved with NixOS.
NixOS boots into Gnome desktop environment! Yay! My external wifi usb dongle D-Link DWA-121 is instantly recognized. Awesome! I can connect to my wifi and begin the installation.
I start GParted and erase all windows partitions. Then I exit the program.
I check my disks with the lsblk command in the terminal and there it shows my disk.
I used to have NixOS with zfs but I haven't learned anything about the filesystem. This time I go for the encrypted Btrfs root and unecrypted 10G of swap partition and a boot partition. I follow this nixos on encrypted btrfs. This time I would like to learn more about filesystems too.
I am surprised at how fast the installation goes, I follow all the steps and then I simply add a user and some minor settings. I nixos-install and then it boots right into NixOS! Wow!
But now, now the adventure truly begins!

Here is my simple configuration.nix


    # Edit this configuration file to define what should be installed on
    # your system.  Help is available in the configuration.nix(5) man page
    # and in the NixOS manual (accessible by running ‘nixos-help’).

    { config, pkgs, ... }:

    {
      imports =
        [ # Include the results of the hardware scan.
          ./hardware-configuration.nix
        ];

      # Use the systemd-boot EFI boot loader.
      boot.loader.systemd-boot.enable = true;
      boot.loader.efi.canTouchEfiVariables = true;

      nixpkgs.config.allowUnfree = true;

      networking.hostName = "lapchi"; # Define your hostname.
      # networking.wireless.enable = true;  # Enables wireless support via wpa_supplicant.
      networking.networkmanager.enable = true;

      # Set your time zone.
      time.timeZone = "Europe/Zagreb";

      # The global useDHCP flag is deprecated, therefore explicitly set to false here.
      # Per-interface useDHCP will be mandatory in the future, so this generated config
      # replicates the default behaviour.
      networking.useDHCP = false;
      networking.interfaces.wlp0s20f0u2.useDHCP = true;

      # Configure network proxy if necessary
      # networking.proxy.default = "http://user:password@proxy:port/";
      # networking.proxy.noProxy = "127.0.0.1,localhost,internal.domain";

      # Select internationalisation properties.
      i18n.defaultLocale = "en_US.UTF-8";
      console = {
        font = "ter-i32b";
        packages = with pkgs; [ terminus_font ];
        keyMap = "us";
      };

      # Enable the X11 windowing system.
      services.xserver.enable = true;
      services.xserver.libinput.enable = true;

      # Enable the GNOME Desktop Environment.
      services.xserver.displayManager.gdm.enable = true;
      services.xserver.desktopManager.gnome.enable = true;

      # Configure keymap in X11
      services.xserver.layout = "us";
      # services.xserver.xkbOptions = "eurosign:e";

      # Enable CUPS to print documents.
      # services.printing.enable = true;

      # Enable sound.
      sound.enable = true;
      hardware.pulseaudio.enable = true;

      # Enable touchpad support (enabled default in most desktopManager).
      # services.xserver.libinput.enable = true;

      # Define a user account. Don't forget to set a password with ‘passwd’.
      users.users.dom = {
        createHome = true;
        isNormalUser = true;
        extraGroups = [ "wheel" "video" "audio" "disk" "networkmanager" ]; # Enable ‘sudo’ for the user.
        group = "users";
        home = "/home/dom";
        initialPassword = "nixos";
      };

      # List packages installed in system profile. To search, run:
      # $ nix search wget
      environment.systemPackages = with pkgs; [
        vim # Do not forget to add an editor to edit configuration.nix! The Nano editor is also installed by default.
        wget
        firefox
        tree unzip unrar
      ];

      # Some programs need SUID wrappers, can be configured further or are
      # started in user sessions.
      # programs.mtr.enable = true;
      # programs.gnupg.agent = {
      #   enable = true;
      #   enableSSHSupport = true;
      # };

      # List services that you want to enable:

      # Enable the OpenSSH daemon.
      # services.openssh.enable = true;

      # Open ports in the firewall.
      # networking.firewall.allowedTCPPorts = [ ... ];
      # networking.firewall.allowedUDPPorts = [ ... ];
      # Or disable the firewall altogether.
      # networking.firewall.enable = false;

      # This value determines the NixOS release from which the default
      # settings for stateful data, like file locations and database versions
      # on your system were taken. It‘s perfectly fine and recommended to leave
      # this value at the release version of the first install of this system.
      # Before changing this value read the documentation for this option
      # (e.g. man configuration.nix or on https://nixos.org/nixos/options.html).
      system.stateVersion = "21.11"; # Did you read the comment?

    }

Haskell day 85 - counting, describing type and function spaces

domagoj miskovic — Thu, 04 Feb 2021 05:02:53 +0000

Types

This post explores the types and functions tutorial by @typeclasses. Their tutorials have this a bit different kind of teaching method, besides pure formalism they seem to try to teach by talking about things, but then at the same time thinking with and through types seem to be very conducive to a different kind of teaching method, different kind of wisdom in which without explicitly stating the set of instructions, for example what needs to go where and when, without merely pointing into the horizon, types take on a much more receptive role and invite the student and the teacher to a different kind of mental state, a much more intuitive, slower state in which there seems to be much more thinking involved within more precisely formed units. Also each definition could have an infinite number of teaching methods or vehicles which might illuminate certain aspects of it, at the same time there is an infinite number of past or future analogies one could use, for example think of the identity or a boolean value. Still, at the same time because of the functional purity and referential transparency and because no information seems to be discarded within imperative lossy flows, higher and more complex abstraction could be realized by composing these basic abstraction units. So something such as a functor is essentially one of the most precious things there is, and once a student learn about these transformations the student realizes that there are more of those types of transformations. Upon realizing such structures an emotional inspiration arises precisely because these abstraction contain themselves within themselves, so to say they scale perfectly in unison, and so one feels empowered more and more while retaining knowledge to a much higher degree, essentially purifying the view within the mind, or to use the term garbage collecting any knowledge. You could say there is not much garbage to be purified while thinking in pure functions since each and every one of them, totally return what they are asked for.

We can think of types as being like sets. When we think about numbers, for example - "numbers" is not itself exactly a set. There are different sets of numbers that are useful for different things.

But this brings to mind that there might actually be an infinite limitless number of these sets of numbers, because there are so many ways to count things, some more, some less useful than others. Besides the usefulness of a counting action, the process of numbering things or objects, we also can analyze how many there are ways to count. But then comes the question could there also be a way to count a finite set of numbers using an infinite amount of numbers, basically never reaching the last finite number of the set? But why would anyone do that? This could be like using every possible real number from the number line to count from 1 to 10, we might never reach even the number 2! We notice there is a certain shape how the counting process evolves, what is this actual movement of the counting process, some numbers seem to flow so to say evenly in the sense that there seems to be an equal distance between each numeral of the counting range, like from 1 to 2, from 2 to 3 and so on while some numbers seem to progress in a different way, seemingly going deeper as in 1.1, 1.11, 1.111.. but then I wonder is this really counting? I read about surreal numbers which are like progressing in a really fascinating way, like they have dual nature, one part of them counts in one way, the other one in a different and both parts of one number consist of one count, as if one number had two numbers within in order to make the count, but I should read more about these surreal numbers, I have no idea how they work. Still sometimes we take for granted the notion of a number and we spend our lives counting with naturals but there is nothing natural about natural numbers, even the name seems confusing at first, why are they called natural, is it just because we have five fingers on each hand? Or twelve little joints on each hand too?

Still to continue the pursuit, if there are numerous ways to count things, and if there are numerous sets of these numbers then there are also an infinite number of types as well! But still, the mere mention of a certain type we seem to forget about the size of the set but begin to think about what such a set could contain, how could it be described, because types seem to be described in a much more detail than just a simple number.

What we call numbers are not a fixed set of things, but a group of sets that have some things in common. For example, we can do addition with members of any of these sets - we can add integers, we can add natural numbers, and we can add rational numbers..

So there are all these operations which we can use with different kinds of numbers, which in turn produce different results, depending on how we want to count something. Hmm, what about these operations then? So there are different types of numbers, different types of things which could have potentially an infinite number of operations defined over them so that means there are also types of collections of operations that could be defined over our space of a variety of number types. How would

Now comes the kicker. In the next paragraph it says that In Haskell, the concept of "being a number" is represented through a typeclass. OK, I actually thought that the concept of a number would be represented as a type since for example a type natural contains all the naturals and a type rational contains all the rational numbers and so on but here I stumble on something else. It continues with We have types in Haskell which are like sets, and we have classes - which is sort of a larger concept - that defines some operations that multiple sets have in common.

Fascinating! So basically types are just like images, or like certain actors within some domain and a typeclass is like a collection of these types, these actors and some number of operations or events that are possible to happen between them. So in our number case the type would be a natural or a rational and these types of numbers would then belong to a larger all pervasive Num typeclass, which is a collection of different types of numbers, different instances of one typeclass. The unique thing that connects them is simply that they are all types of numbers with some operations defined over these numbers because we need operations if we want to do something else besides simply counting from the lowest to the highest number. We naturally come to define other operations when our conditions change. If we were to count how many people are in a room we would start counting 1,2,3 until we reach the last person and so on but if suddenly 10 people were to leave we might just want to simply subtract those 10 from the total number of people instead of counting again from the beginning. This is especially useful if there are a million people in the room and 10 people leave, who would want to start the count all over again? But then does the computer actually count again from the beginning? Is a list of people being counted from the beginning and then if some are to be erased will the computer count again from the beginning? How does the program count the list of people then if it can't see that 10 people are missing from the room? This is a question that has to do with how lists, a basic data structure is implemented and how the computer constructs these structures.

What if you could not count at all? What would be the simplest possible way you could count things? You could simply say a word, like "DA", and then "DA" over there, and then "DA" and all the numbers would be "DA". This is very simple, like seeing every thing in the world as a toy you reach out point towards it and happily say "toy!", this is a "toy"! and so on. So this is like a type that is not numeric in the previous sense but that has only two values within, called Bool. So instead of DA this type can describe things with True and False which actually seems like the minimum amount of abstract movement one can make within ones mind. Something could be here or there, something could be true or false, but is it really like that? Is our Bool something like a simple DA? Well maybe it is not, since it contains two symbols. The DA would seem to be some kind of identity which does not even affirm the thing being pointed at, it merely repeats the same thing over and over again without regard to which thing we provide it. So if we give it an apple it says DA, if we give it a string it says DA, is this some kind of an identity? But an identity would be like identity :: a -> a and in our case this seems more like da :: a -> da. What is this then? Aha! This might be that super cool type called Void which always returns void. But why void, is it because it makes no sense and only introspects within itself like a black hole, like some void without any bottom anything that we throw at it becomes simply void? So like DA, void is a form of DA, fascinating!

But can we think of a typeclass, maybe, that could include both character types and numbers? What could a set of characters and a set of numbers have in common?

Yes! When we use numbers we often like to use words too, words that have meanings so what would such a type look like that would contain both words and numbers within. One needs to be a bit more precise because when we say words and numbers what we actually mean are characters and numbers, because characters form words not the other way around, but then some words do form our character too, now that might be confusing, but so words are, they are awfully confusing with many meanings! But let's come back to the question of What could a set of characters and a set of numbers have in common? Well this is deep, I am kinda staring into the darkness and thinking...

So I look into the other window and there it says,

...they can be put into an order. There's a typeclass for that, called Ord. That's where the comparison operations like greater thn (>) and less0than (<) are. One value is less than another (x < y) if x comes before y in ordering.

Now what is actually happening here? We are actually not counting now but it seems to me we are arranging the counting numbers into an order, as if we already did the count and now the numbers got all mixed up so we rearrange them again into the counting order. But the thing with order is that it seems we do not have to do the count again, we just have to order them, we put the smaller number before a larger number or maybe do any ordering operation we like. Why are we ordering things? Well we order things all the time, even our thoughts come completely in an unordered form in o ur heads and then we suffer mentally because we are unable to order our thinking so that we don't suffer. Maybe all suffering consists of unordered thought and our brains which love types and mathematics cannot stand that, they cannot stand that some thoughts are larger and some are smaller and then it wants to order things. There is something beautiful and all encompassing when we look at an ordered field, it somehow looses the individual particularities, those numbers that jump out or fall back. An ordered field is like an empty space, each individual unit is like being aware it is a part of something greater than itself, each number is at the right place at the right name. We also understand things much better when we order them and have a better sense of their individual characteristics when we order them.

But what happens when we see two instances of the same number, of the same thing in front of us, is this even possible? What if there are two equal things or isn't everything actually unique in itself? Are two oranges equal? Well if we are simply counting 2 oranges and 10 apples then maybe yes two oranges are equal and 10 apples are equal, it seems it all depends on what kind of an abstraction level we are standing upon. Some things seem to be equal and then those same things are not when we look at it from a different poin of view. Equality seems like a super deep question, that might be the last question there is? Could it? Well Haskell has an equality class of types called Eq which has an operator == which is tests for equality. But what is the difference between the double == and a single =? A single = seems to be forcing us to observe some result from some action while == is like simply measuring if two sides of an equation are the same. But then why the equations I did in the elementary school contained only a single equality sign and not ==? Maybe because the result was being mixed with the action itself, so some unknown variables were being added and then the result was also intermixed with some extra variables, the result was hidden, obscured so we had to extract the single unknown variable which was the result. This still seems different than the double equality sign. But then how would you judge what is equal, it seems there are infinite levels of double equality signs, meaning there are all kinds of equalities around, some more tight some loose to use a slightly loose terminology...

Functions

Now if types were to be understood as concrete images then functions would be like moving images, like movies of those images, just in our case our movie could be arranged in all kinds of ways, we would not have to go only from the beginning to the end but we could like in the recent Nolan movies Tenet go back and forth in time while at the same time some other timeline could meet us in the future. We could arrange our images into whatever we want because we are not bound by the meaning of these images. When we describe a meaning it is usually set in some temporal shape, into some timeline, this is what meaning basically means, but then the more actors we perceive, the more events we engage with the more our timeline warps into itself and introduces different time-shifts within. OK, so what are functions, these super exciting movable objects. Wait are functions objects? Or are they functions? A function is more like an action, so how would we compare an action with an object. Well maybe if we understood an action as an transformation then maybe we could call that particular type of a transformation an object? Hmm..

On the left we have numerals, on the right we have the words for numbers, and we are asked to draw a line from each numeral to how it's spelled. In our elementary schools we had to do a lot of these kinds of exercises. This is our mental picture of what defining a function is like: drawing lines from the things on the left to the things on the right, based on some rule that tells us what makes the matching meaningful. A function is a description of how an element from one set gets matched to an element in another set.

This is a really nice description of how a function works. Let's check the Wikipedia one which is a bit more formal but still the same:

A function is a process or a relation that associates each element x of a set X, the domain of the function, to a single element y of another set Y(possibly the same set), the codomain of the function.

The one before that is also a bit more compact:

a function is a binary relation between two sets that associates every element of the first set to exactly one element of the second set.

But let's return to typeclasses where a simple program is introduced! Yay enough theory!

spell :: Integer -> String

So the spell is the function name then the empty square with only corners shown or a double colon sign which symbolizes the action of saying has a type or basically what the double colon means is that it is raising the abstraction level from naming things into describing which kind of processes are to be uniquely identified with that name, so could our spell be actually an object? Could this spell function be understood as an object? Why? Because it has a name? Is every thing that has a name an object too? OK, so what does Integer and String represent here, they represent the domain of our process and the codomain, which is like the starting point of our transformation and the endpoint of our transformation. Now it might be the truth that actually the domain and codomain are basically the same thing, though they might seem different if we look at it from a temporal perspective, after all a broken egg is still an egg but it is broken only after and not before so some kind of transformation did take place. So is it then breakfast :: whole egg -> broken egg or maybe sunny side up :: whole egg -> broken egg? But let us continue with the typeclasses code example:

spell :: Integer -> String

spell int =
  case int of
     1 -> "one"
     2 -> "two"
     3 -> "four"

to be continued...

day 86: a semigroup of haskellers and a logician walks into a bar

domagoj miskovic — Sun, 13 Dec 2020 07:59:35 +0000

It is 2018. I live in New York City and I am going to NYU to hear a lecture on semigroups, lattices and duality by a visiting expert in the field, who came over from Amsterdam. After the lecture we talk about music composition and some weeks after begin to exchange emails about math and music, he wonders what is music, what does it all mean, what is its connection to math? He seems super nice. The four hour long lecture is a part of an ongoing series of meetings by local mathematicians, category theorists and functional programmers, mostly Haskellers from the local Haskell and lisp meetup. I am happy, amused and excited by the gathering especially since I do not understand almost nothing being said. But I hold my attention for the whole duration and keep my mouth and my mind shut completely. I hold my gaze at the lecturer and carefully observe what is happening in the group giving it my full attention by taking away any obscuring thought I could have at that moment. You could say I meditated, tried to remain calm with concentrated awareness.

Why am I interested in abstract non sense? I am a trained classical musician, since early childhood, and have practised an instrument for long hours every day. I practised the art of listening for long durations, listening to sonic relations which have no apparent semantic meaning, at least not any common, real world semantic meaning that I know of. A sonic space does not tell a story although it could, no, it is defined by sound, by how the sound moves, as if the sound itself is some kind of life-form that speaks a language unknown to you, but you can listen to it and the best of all, strangely it can make you feel! Most of all you do not criticize it and find errors in it, the better you get the less wrong notes sound like wrong notes, and more like interesting occurrences. These feelings are the same ones you know but there are also subtle ones, that can only be described by words such as sublime and grace. But there is also a deeper semantic meaning to all this, some kind of mathematical structure to it all, something that maps within different regions in the mind, in the body itself. If sound was a type of a body since it has an origin and a trajectory and can be felt, certain relations move within in a variety of ways. There is something deeply intuitive in all this. I wondered about this from time to time, and its not about C majors and F minors, and G minor scales. These are all afterthoughts made to deconstruct this landscape into something tangible, something physical, something to be seen and not intuitively felt.

After the lecture he takes some questions and someone carefully develops for almost 10 minutes one question. The lecturer brushes it off saying: No, this is not that, this is something different. But then the mathematician rephrases it again and yet again the lecturer thinks for a second and says.. no.. its not that too.. it could be this or that, but its not that… He didn't really say this but in some sense he didnt really approach the question inclusively, it seemed he dismissed it as inappropriate for that context.

Among those people is is a cool old logician Jaz Sulzberger who I already met one time in a Lisp meetup, who will give me a lecture of a lifetime on Curry Howard correspondence later in the bar over drinks, when the rest of the Haskellers leave. Some of them seem to be annoyed by his remarks and enthusiasm. I can tell that by the way their faces look down while he speaks about some obscure thing, or begins to inject a variety of related arguments into the discussion. I almost feel sorry for him and at the same time feel inspired by that teenage feeling when being in the presence of a master, when you see no one else, when all you think of is just being in the presence of your master, when imitation is the only form of art you do. When you even try to breathe and make facial expressions as the master. Here is a lecture of his and there are more:

https://vimeo.com/39639153

Here is a picture:

I have studied categories on my own by following Milewski lectures on youtube with great enthusiasm and vigor, drawing diagrams on my two room windows in Brooklyn. There is something strange and captivating about category theory, it seems like a perfect abstract tool, something to be discovered rather than operationally invented. I spend the Summer reading dialogues of Plato and notice abstract structures repeating, similar structural entities in which different arguments are injected, in which truth is told and yet there was an abstract notion of yet another kind of truth, the one not talking about objects at all, but simply talking about kinds of transformations that were happening within that space. But I could not find anything written about those happening. I read Hegel and Zizek too and wonder how cool it would be to put some of the philosophy into code but a notable Haskeller tells me over the table:

"Hey I just hate philosophers, I can't stand them"
"Oh really? How come?"
"I just can't stand them"
I gaze silently at him and hold my drink. I switch them my view to the logician. I was saddened by that response. I was waiting for some discussion. Seems to me functionally strange to hate something..

They all leave after few drinks and I stay there with the logician who tells me a story about the Curry Howard Isomorphism. He tells it like the fate of humanity depends on it, today I need to hear it if I want to save the Earth tomorrow. It seemed so important and his tour de force way of going through that forest of arguments made me mesmerized. Again I did not understand a single word, not that I remember now. But I listened closely to him, I watched him, I felt no fear, no boredom, I just followed the words, having faith that eventually I will learn the language. I felt that intuitive hold on my consciousness, the excitement of listening to something unknown to me, something defined by rich relations, something not plain obvious. I often hear how people have much difficulty in engaging something they do not understand and I find that deeply sad. I guess I felt the it more important to be engaged into something with the whole body and mind then just following along something which merely confirms what I already know.

At the end I tell him, I admit it is all very difficult for me to follow and he tells me like a father, like a close friend:

Hey, don't worry, I didn't understand a thing in the beginning, in time you will know, you will begin to understand. Tell me your name, what is your name.

He wrote my name in his scrapbook and left. I am so grateful to that wonderful logician and I send him warmest hugs where ever he is. Thank you!

Day 87 :: Haskell Holmes tells Watson how to curry sheep

domagoj miskovic — Fri, 06 Nov 2020 14:32:06 +0000

Watson: Sherlock, I've been meaning to ask you something about pure functions. How do you define these functions, I mean I understand that functions and function types seem to be like morphisms, ephemeral entities that transform data like abstract ideas, a structure describing a pure relation, like f :: e -> e, a computational context into another kind of context, at least the higher order functions do that, the ones that take functions as arguments which take functions as arguments...

Holmes:... But Watson all Haskell functions take functions as arguments, it's actually quite simple, we pass functions to one another and solve our problems, the more a problem seems complicated so we call and combine more complex functions, by complex I mean appropriate for that specific domain, or more abstract and structured. The process is somewhat dual to my deductive method, it just begins bottom up instead top down.

Listen Watson, try to follow me now and I will show you how we do that. Imagine you were to just count sheep upon some green hill, imagine yourself as a shepard counting sheep, and please Watson try not to fall a sleep. So you see a sheep, call it a and count one, then you call a function, call it f, which adds numbers. How does it add numbers? Well it is defined by a method you could say, like a method that describes a typeful operation, (+) :: Num a => a -> a -> a. Now this function adds numbers, it is a method to add things. If you observe the method carefully you will see that the plus sign, (+), is constrained to an operation, defined to add numbers, all the numbers which belong to a whole class of number, so (+) :: Num a would mean just that. The rest of the declaration says that the plus function takes an a variable and returns a variable a and then returns another variable a, more correctly said a plus function takes a variable and returns a plus function that takes a variable and returns the result. We can visualise this as (+) :: Num a => a -> (a -> a). Notice the beauty in the fact that plus is defined over numbers and yet we can use it to count sheep, how great is that?! Now forget all that mambo and remember we just saw the first sheep and we have an idea of a number, number 1, now what do we do?

Watson: Well we look at some other sheep, preferably the one next to it and count that one as two.

Holmes: That's brilliant Watson, please fetch me some tea from the replicator! Tea Earl Grey, hot! Well Watson, that is true but try to look beyond, try to abstract away the whole process of counting, it makes no difference that we are counting the sheep next to that first one as number two, and also Watson, there is something dark and sinister happening here. Imagine that you are an idiot, a complete idiot and that you had no idea how to count, imagine that! Haha! What if we could not count?! Imagine you had no idea to count at all, could you? What would you do then?

Watson: So I have to count sheep but at the same time I cannot count, I don't have the slightest idea of how to even begin to count? I guess I would call someone who could count for me, who would know how to count? Someone like you naturally I presume?

Holmes: Well yes, but you might be taking this game a bit too far into the concrete realm, now imagine you cannot count, so as you say you would call me. Could you say you would call some function be it me or someone else to count the sheep for you? A function after all is some morphism that transforms data, it is more than just a value, it takes a value in and produces a value, it returns a value, and it always returns the same value if it is provided with the same input value. Our function is a pure function, it is defined totally over the whole space of its arguments! I mean if we provide our function two sheep it better count them one, two, equals two right? It's just now quite like that you will find out, the function will simply take one sheep and output another function which will return the one plus the second sheep. But I am getting a head of myself, like taking a head of an empty list it is too early for you to understand what is going on. Just follow along!

So to get back at our counting adventure you count one sheep and than you call me or let's say our holmes function and ask it to count for you. Now what does the holmes function do then? It simply takes the second sheep as its input and returns another holmes function that takes the third sheep as its input which then again calls another holmes function which takes the fourth sheep as its input and then again, it returns a function that takes...

Watson: But wait a minute Holmes, so who is counting? And it seems to me each iteration, each new number we have another function, replicating itself, just taking the next number in line, but still no one is counting, I mean I still do not how many sheep there is in total? Also I don't think I can handle more than one Haskell Holmes, and now you are telling me there are a bunch of them!? Which one is going to sum up the whole list of these sheep??

Holmes: No worries Watson, my replicas will vanish as soon as the calculation finishes, except if you memoize me somewhere within a cache field, then I will remain for some time until you call me again. But never mind that, we will talk about memoization some other time, it is a quite fascinating idea! So basically, we call a new function for each number we add, passing a function to a function we share information, we do not count yet, or sum these numbers why would we? After all we must collect our 🐑 first, we must collect our objects before we add them. You see if we were to begin adding these objects immediatelly we would be making destructive updates creating state along the way and tell me where is the rush, if we want to be correct, truly correct and sure in what we are doing then we must collect them all and then sum them up. It is just our mind that immediatelly sums up these numbers and because notice Watson the number itself is actually the sum of all previous numbers. Look at it, the sheep number 5 tell us not just that bit of information but that actually each number is a sum of all the previous numbers, have you noticed that? Have you?

Watson: Oh my god, so a number 10 is actually the tenth number and at the same time the sum of previous numbers? But isn't the sum of all previous numbers from one to ten, something else? sum [1..10] is not 10?

Holmes: Watson that is true but you are actually playing a smart boy now, because the correct list of an unknown number of sheep would be [sheep, sheep, sheep, sheep, sheep, sheep ...] or to use a variable instead we have a list of things something like [a, a, a, a, a, a, a, a, a ,a]. Do you see the difference? Now we have lets say ten individual units, ten a's which if we sum, if we add together we will get 10, but this does not apply to your example because summing numbers from one to ten is a bit different, a more abstract situation, because you already know the numbers you got, if would be like adding one sheep then adding two sheep, then adding three sheep on that hill over there, than imagine you had four sheep over there, look there, a bit further away, then look you have five sheep over there! How would we describe this?

(+) [1..10]

{- let us unfold the list into its elements, 
[1, 2, ,3, 4, 5, 6, 7, 8, 9, 10]

1 + (2..10)
1 + (2 + (3..10))
1 + (2 + (3 + (4..10)))
1 + (2 + (3 + (4 + (5..10))))
1 + (2 + (3 + (4 + (5 + (6..10)))))
1 + (2 + (3 + (4 + (5 + (6 + (7..10))))))
1 + (2 + (3 + (4 + (5 + (6 + (7 + (8..10)))))))
1 + (2 + (3 + (4 + (5 + (6 + (7 + (8 + (9..10))))))))
1 + (2 + (3 + (4 + (5 + (6 + (7 + (8 + (9 + (10)))))))))
1 + (2 + (3 + (4 + (5 + (6 + (7 + (8 + (9 + (10 + ()))))))))
1 + (2 + (3 + (4 + (5 + (6 + (7 + (8 + (9 + (10 + 0))))))))
1 + (2 + (3 + (4 + (5 + (6 + (7 + (8 + (9 + 10))))))))
1 + (2 + (3 + (4 + (5 + (6 + (7 + (8 + 19))))))
1 + (2 + (3 + (4 + (5 + (6 + (7 + 27))))))
1 + (2 + (3 + (4 + (5 + (6 + 34)))))
1 + (2 + (3 + (4 + (5 + 40))))
1 + (2 + (3 + (4 + 45)))
1 + (2 + (3 + 49))
1 + (2 + 52)
1 + 54
55

Take a look at this beauty Watson, enjoy this linear recursive process! And mind you a list is a collection of homogeneous entities, meaning they are similar and uniquely different, you could say they have the same type...

Watson: This calculation is amazing Holmes, and just look at it, how the program expands in time and space! How did you do that? But it looks awfully difficult too. I think I can manage to process until it unfolds completely, but then how do you put the numbers together, I mean it seems this is much better suited for computers than humans, but then again this process precisely describes the whole act of counting sheep! And somehow we are fully aware of everything what is happening at every step of the way. I imagine if we merely destructively updated the state with a counter it would look much simpler and yet all the magic would be hidden away! But wait a minute, this is not quite right, how would we sum just a bunch of ones?

1 + (x)
1 + (1 + (x))
1 + (1 + (1 + (x)))
1 + (1 + (1 + (1 + (x))))
1 + (1 + (1 + (1 + (1 + (x)))))
1 + (1 + (1 + (1 + (1 + (1 + (x))))))
1 + (1 + (1 + (1 + (1 + (1 + (1 + (x)))))))
1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (x))))))))
1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (x)))))))))
1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (x))))))))))
1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 0)))))))))
1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 1))))))))
1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 2)))))))
1 + (1 + (1 + (1 + (1 + (1 + (1 + 3))))))
1 + (1 + (1 + (1 + (1 + (1 + 4)))))
1 + (1 + (1 + (1 + (1 + 5))))
1 + (1 + (1 + (1 + 6)))
1 + (1 + (1 + 7))
1 + (1 + 8)
1 + 9
10

Watson: So a list is a collection of numbers? What is its type, a number?

Holmes: Not quite, a list is a collection of objects, which yes are similar which yes could be numbers, but could also be sheep! We used the numeral 1 to count our sheep but really Watson is that even necessary at all? I mean you could use the variable, a letter s for all I know and it would have been the same, we would still have to write 2ss, 3ss, 4ss, because when you add a letter s, or let's better call it a character s to a character s you get ss or you could also say you get two ss, it's just it is more convenient to use numbers, at least for now while operating on the term-level. Mind you working at the term-level is not for everybody, people get hurt here, they leak memory etc. It's gruesome and bloody!

Now tell me what type is a sheep anyway? Some kind of an animal right? A sheep is not an Int, or an Integer, right? Which means a sheep does not belong to a Num class of numbers, of which certain kinds of number are only instances of this large class of numbers. We have Integer, Int, but we also have Float and Double and hey you could define any number you like, I myself am intrigued by surreal numbers, I fell in love the moment I heard about these wondrous entities, they seem to encode more information within, but more on surreals some other time! Watson, please notice that the whole idea of a number comes from ordering things, after all you are aware of some order, meaning the idea that some things come before or after some things, after all how do we measure time? One second passes, two second passes, one minute...

Watson: After all what are we doing thinking about programs all the time, yes we write our cases, and explain our steps and people read our stories and follow our investigations but at the end of the day what is it that we do actually?

Holmes: You find yourself perplexed again my Watson, by the wonderful world of programs, they seem elusive, no matter how hard we try to encode these entities into our frameworks a bitter taste remains, something again to strive for, some new algorithm, but honestly aren't you bored sometimes by the..

The baby is crying, and it is time for a bath, I enjoyed this a lot, I hope you did too...

Indiscernible types of Haskell Holmes

domagoj miskovic — Thu, 05 Nov 2020 08:12:19 +0000

There seems to be an ambiguity in the idea, a common vibe I hear on the grid, like an excuse mentioned in some books and papers, that one of type safety's downsides it the fact that some expressions which would otherwise evaluate to a true value would be rejected on the typing grounds, the reason being that even though for example both expressions in an if then else may on their own evaluate to true or to some true value within a known type instance of their own, they somehow cannot exist together in a branching statement, one cannot call another one, meaning if such expression is true then this expression is true, meaning the second expression will take place, the second event will happen if the first evaluates to true, as if this new event that may take place is to be rejected simply because it does not follow the type in the first expression. The common example would be if True then 1 else False where if some boolean value in the Bool class of type values which contains two values True and False or a boolean function type such as not :: Bool -> Bool which is a function from one bool to another bool, sou see when you negate something you get the inverse of that thing or something else within that type universe, what else could it be? Not true is false, negate 5 is -5... now if such an expression evaluates to true we are to call a number, or any number, in this case an integer number, 1 :: Integer that belongs to a class of numbers, 1 :: Num p => p but you know all that. Apparently this seems to be an invalid statement, an invalid type inference between two expressions, between a bool and a number one.

Watson: Hmmm... what if instead of False we would have something like otherwise "play me an ambient like Jedimind soundtrack now"? Would that be any different than a simple False. What is happening here and why is this a bad thing in the first place?

Haskell: But Watson, my dear friend it is not about the rest it is about creating algebraic structure with not enough information.

Watson: What information? If something is true then give me 1. What is so strange about that. You seem to question everything, I am not surprised you named your dog Haskell for all I know.

Haskell: Watson I do not have a dog, you would be the first to know if I had one.

Watson: There, you just said if you had one I would now, could we take that as an example?

Haskell: Watson my boy you cannot just jump from one to another mathematical realm and expect not to spill any milk along the way. The obvious reason your reasoning is currently at its peak is that you are not fully aware of the way types transform from one instance to another.

To put it simply, the way a computation evolves depends on the language your structure encodes and the way to compose different structures into new ones you will have to do a lot more than a simple if then else statement! Try to see, if then else statement if we translate it into a typful universe might seem like an instance of a boolean function. I am describing it as a boolean because it is so simple, it actually goes from a bool to a bool. But hey we are Haskellers, and this is an old artefact from medieval times, I suggest you practice defining functions without such if then else statements because Watson my friend life is complicated and no if then else statement is going to save you from your puny little brain, even worse you might have to stitch together a string of such expressions, then when you look at it, you will not know right from wrong.

Watson: All right Holmes, and tell me what about the Either type? data Either a b? It also seems like an if then else statement with maybe more freedom defined since either a or b is for you to pick which could be also realized if True then a and if True then b. How about that?

Haskell: Bravo Watson, you did it again! Eitherdata type does represent either one value or another, Either a b which we can further realize as Left a| Right b and it might seem like we take these lefts and rights for granted while if we had an if then else before either, we would be actually checking some precondition and then applying one of these eithers.

data Either a b = Left a | Right b

firstCondition = Left True
secondCondition = Right 1

Watson: This is beyond me Haskell, how did you come up with this?

Haskell: My dear Watson let us go then you we must investigate this case immediatelly! Call a cab!

88th day Haskell meditations: substitutions, structures, identity of a monoid

domagoj miskovic — Tue, 03 Nov 2020 13:11:47 +0000

I realize that more and more as I learn Haskell, as I think through it and with it, that most of my time programming, what I really enjoy doing, what keeps me at bay or at the sea of simulation, what inspires me to program, to code, is not actually solving a given problem within a specific domain space but exploring what it means to compute, to reason computationally, to think recursively. I find myself visualising in my mind how a program looks like in time and space, how the computation evolves, how the substitution applies, how equivalences are compared, defined by various morphisms I learn to define, how seemingly simple operations I took for granted in my elementary school days are transforming, they remain the essence in forming structures of contexts that seem fluid, defined out of time they directly give it a unique description. After much pondering and wondering about such structures you naturally begin to feel the urge to reach into mathematics which abstractly deals with these entities. You might not know you are doing mathematics, but soon enough you will.

In mathematics such structures are called algebraic structures, which are described as structures with an additional context, a behaviour or a class of behaviours, behaviours being some operations, like a program we can realize these algebraic structures, differentiate between their properties and compare them as well. Many have real world examples but often the human mind is blinded by the example itself, a finger pointing towards the moon, the moon in our case being the essence of the object, stripped out of its concrete implementation in real time and space its abstract shadow looms over it, functionally describing its sequence of operations.

Let us take a simple operation of multiplying and adding three numbers such as: 3 * (5 + 9). This example which is from "Haskell School of Music" book is showing the basic abstraction principle happening. We will not "solve" this (the result of 3 * (5 + 9) = 42 but try to see how to abstract this whole operation, this set or a collection of two operations into a function called simple which will compute the result for us. We will think about how the computation unfolds rather than just calculating the end result.

We can realize that we have two operations in place happening here and three variables, context holders which are already substituted for real numbers. So let us abstract these numbers away and just write a * (b + c) or even x * (y + z) because we would like to see how the function works an any three numbers, at least for now let us remain with whole numbers, numbers which are familiar to us.

But where is the simple function? We only see the (*) and (+) operators between three variables in an infix position, infix positioned meaning between, inside of some expression while prefix positioned meaning before the expressions, at the beginning, something like this: (+ 1 2 3 4 5) or like this: sum [1,2,3,4,5,6] or shorter sum [1..100].

We will simply call our function simple. This function will take three variables x y z and its body will be defined like this: = x * (y + z). Notice the left side of the equation, the list of parameters the function simple and how there are no operators. Only in the body of the function we describe the operations.

simple x y z = x * (y + z)
simple 3 5 9 = 3 * (5 + 9)
             = 3 * (5 + 9)
             = 3 * 5 + 3 * 9
             = 15 + 3 * 9
             = 15 + 27
             = 42

Notice we used the "multiplication distributes over addition" property which seems quite natural to us:

During mental arithmetic, distributivity is often used unconsciously: 6 ⋅ 16 = 6 ⋅ ( 10 + 6 ) = 6 ⋅ 10 + 6 ⋅ 6 = 60 + 36 = 96. Thus, to calculate 6 ⋅ 16 in one's head, one first multiplies 6 ⋅ 10 and 6 ⋅ 6 and add the intermediate results. Written multiplication is also based on the distributive law.

But a bit later in the book there is an exercise left for the reader, which says: simple (simple 2 3 4) 5 6 What is happening here? It seem like the function simple is applied to one of the three variables, meaning we are passing that very same function back to itself, using the result of that function, holding it, and then putting it into the simple x variable itself. Notice even the variables we use are not the same, meaning each instance of the simple function has their own set of input variables. So we have:

simple x y z
-- into the x we put another function simple x y z
simple (x = simple x y z) y z
simple (simple x y z) y z

simple ((x * (y + z)) y z
((x * (y + z)) * (y + z)
(x * y + x * z) * (y + z)

But maybe we could even take a simpler example, an example of doubling a number with itself, adding it to itself or multiplying it with 2. And we will call our function double:

double x = x + x
double 2 = 2 + 2
         = 4

-- or with lambda notation
double = \x -> x + x
double 2 = (\x -> x + x) 2
         = 2 + 2
         = 4

In computer science, many abstract data types can be endowed with a monoid structure. In a common pattern, a sequence of elements of a monoid is "folded" or "accumulated" to produce a final value. For instance, many iterative algorithms need to update some kind of "running total" at each iteration; this pattern may be elegantly expressed by a monoid operation.

This description of a monoid makes me think on how keeping the running total of for example some elements in a set, or objects in a category, or points in a space, or even observing stars upon the night sky, also thinking of how many seasons ago, how many years ago, how many birthdays ago, is like counting some quantity, like counting the times of some event, using the numbers to track of how many days since or how many nights more, seeing it on an analogue or a digital time keeping device, a clock, any kind of device which would measure time through cycles, returning to itself, touching the zero, zero, 00, or the twelve hours place, or the twenty-four, the identity. Its seems quite intuitive for us when observing time on a time keeping device to instead of saying 10 + 4 = 14 to say 10 + 4 = 2 meaning 10 hours + 4 hours tracks the time, over twelve, the 0 element, the identity of one day or night, or more correct a 12 hour cycle gone by, into a new cycle of a new running total, a new count, which would be 2. Yes, there is a difference between a 12 hour cycle and a 24 hour cycle which would seem to have two kinds of identities but more subtly the 24 hour mark is like a binary relation, the second subset of elements within a some set: {12,24}

A number of countries, particularly English-speaking, use the 12-hour clock, or a mixture of the 24- and 12-hour time systems. In countries where the 12-hour clock is dominant, some professions prefer to use the 24-hour clock. For example, in the practice of medicine, the 24-hour clock is generally used in documentation of care as it prevents any ambiguity as to when events occurred in a patient's medical history.

The idea of an identity seems unnecessary when observing identity :: a -> a which is just a function pointing to itself, an object pointing to itself, but seen in isolation almost with a kind of deep lens we might miss the implication of the identity element and its function. If we think about the operation of summing some numbers, adding them together we know that if we add a zero to any number we get the same number back:

0 + 1 = 1
0 + 2 = 2
0 + 3 = 3
0 + 4 = 4
0 + 5 = 5
...

We see the pattern that the same number returns when we add a zero to it. So this means that when we add a 0 to any number, and we will use a variable n or x as a context holder, a variable which may represent any number in our number system, again, we get the same number. Mathematically, it could be said:

An additive identity is the identity element in an additive group. It corresponds to the element 0 such that for all x in the group, 0 + x = x + 0 = x.

So 0 + x = x + 0 = x simply means that 0 + any number x is the same, or equivalent to adding that same number x to a 0. What just happened? We just switched sides like 0 + x into x + 0. What does that mean?

In mathematics, a binary operation is commutative if changing the order of the operands does not change the result. It is a fundamental property of many binary operations, and many mathematical proofs depend on it. Most familiar as the name of the property that says "3 + 4 = 4 + 3" or "2 × 5 = 5 × 2", the property can also be used in more advanced settings. The name is needed because there are operations, such as division and subtraction, that do not have it (for example, "3 − 5 ≠ 5 − 3"); such operations are not commutative, and so are referred to as noncommutative operations.

Because it is both at the same time and it is encoded with that extra bit of information of pointing to itself. This kind of a mathematical structure is called a monoid. We can then realize monoid as an object within a algebraic space of such objects.