Basic unit type:
λ> replTy "()"
() :: ()Basic functions:
| module FizzBuzzC | |
| %default total | |
| -- Dependently typed FizzBuzz, constructively | |
| -- A number is fizzy if it is evenly divisible by 3 | |
| data Fizzy : Nat -> Type where | |
| ZeroFizzy : Fizzy 0 | |
| Fizz : Fizzy n -> Fizzy (3 + n) |
Basic unit type:
λ> replTy "()"
() :: ()Basic functions:
nix-channel and ~/.nix-defexpr are gone. We'll use $NIX_PATH (or user environment specific overrides configured via nix set-path) to look up packages. Since $NIX_PATH supports URLs nowadays, this removes the need for channels: you can just set $NIX_PATH to e.g. https://nixos.org/channels/nixos-15.09/nixexprs.tar.xz and stay up to date automatically.
By default, packages are selected by attribute name, rather than the name attribute. Thus nix install hello is basically equivalent to nix-env -iA hello. The attribute name is recorded in the user environment manifest and used in upgrades. Thus (at least by default) hello won't be upgraded to helloVariant.
@vcunat suggested making this an arbitrary Nix expression rather than an attrpath, e.g. firefox.override { enableFoo = true; }. However, such an expression would not have a key in the user environment, unlike an attrpath. Better to require an explicit flag for this.
TBD: How to deal with search path clashes.
This document contains some ideas for additions to the Nix language.
The Nix package manager, Nixpkgs and NixOS currently have several problems:
enableFoo, but there is no way for the Nix
UI to discover them, let alone to provide programmatic ways toI've been fiddling about with an idea lately, looking at how higher-kinded types can be represented in such a way that we can reason with them in Rust here and now, without having to wait a couple years for what would be a significant change to the language and compiler.
There have been multiple discussions on introducing higher-ranked polymorphism into Rust, using Haskell-style Higher-Kinded Types (HKTs) or Scala-looking Generalised Associated Types (GATs). The benefit of higher-ranked polymorphism is to allow higher-level, richer abstractions and pattern expression than just the rank-1 polymorphism we have today.
As an example, currently we can express this type:
First off, thanks for all the comments and kind words on the original writeup; I've been meaning to follow up on some of the suggestions and write about the different ways to represent monads (and functors, HKTs, etc) that now exist, but a month of being busy has kind of gotten in the way (mainly with three new kittens!).
And for sure, I do not expect (nor do I want) this to become the norm for production-level Rust: rather, I hope that this can contribute to the foundations of programming with higher-level abstractions in Rust, somewhat like how early template metaprogramming in C++ and typeclass-constraint-unification metaprogramming in Haskell have contributed, perhaps indirectly, to later innovations in their respective languages and ecosystems that were much more reasoned, sound and usable.
One of the things suggested in the com