clean up old stuff

README.md

@@ -25,13 +25,13 @@ Example
 ~~~haskell
 ( a -> Bool ) -> [ a ] -> Bool
 
---└────────┘  ↑          ↑           
+--└────────┘  ↑          ↑
 --    |       |          └── final return value is a Bool
---    |       └── The function returns a function that takes a list of type 'a'      
+--    |       └── The function returns a function that takes a list of type 'a'
 --    └── function that takes an 'a' and returns True or False (Boolean)
 ~~~
 
-> [!TIP] 
+> [!TIP]
 > Prefer Type variables (`a`, `b`) over using the `Any` keyword.
 
 > [!TIP]
@@ -48,8 +48,16 @@ Arbitrary Sets or Lists can be denoted with the `...` operator:
 
 { ... }
 
--- ↑           
+-- ↑
 -- └── Attribute Set; where the content is unknown / can be anything.
+
+
+{ ${a} :: b }
+-- ↑
+-- └── Above is equivalent in meaning with this explicit expression.
+-- └── `a` is a type variable. Is constraint to the `string` type, such that it can be used as an attribute key.
+-- └── `b` is a type variable. If constraint in other places it has the `Any` type.
+
 ~~~
 
 > [!Note]
@@ -61,7 +69,7 @@ Arbitrary Sets or Lists can be denoted with the `...` operator:
 
 [ ... ]
 
--- ↑           
+-- ↑
 -- └── List; where the content is unknown / can be anything.
 ~~~
 
@@ -70,23 +78,23 @@ Arbitrary Sets or Lists can be denoted with the `...` operator:
 ~~~haskell
 
 { ${name} :: Bool; }
--- ↑           
--- └── name is of type [ String ]; This list of actual members is calculated at evaluation time. But we know every member has a value of type `Bool` 
+-- ↑
+-- └── name is of type [ String ]; This list of actual members is calculated at evaluation time. But we know every member has a value of type `Bool`
 ~~~
 
 ### 🤕 Bad practice: `AttrSet with multiple dynamic names`
 
 > [!WARNING]
 > The following should be avoided.
-> The confusion arises because we're mixing different types of values in a single structure. It's like having a drawer with both socks and utensils; it's hard to know what you're grabbing without looking. 
+> The confusion arises because we're mixing different types of values in a single structure. It's like having a drawer with both socks and utensils; it's hard to know what you're grabbing without looking.
 
 ~~~haskell
 
-{ 
-  ${name} :: Number; 
+{
+  ${name} :: Number;
   ${version} :: Derivation;
 }
--- ↑           
+-- ↑
 -- └── there are multiple dynamic entries. The keys of `version` mapping to a Derivation each.
 ~~~
 
@@ -107,10 +115,10 @@ The above type is demonstrated in a concrete value.
 Any -> Any
 -- becomes
 a -> a
--- ↑           
+-- ↑
 -- └── This is more concrete. And shows if values relate to each other
 
--- More 
+-- More
 
 a -> b -> b
 -- e.g. builtins.trace
@@ -121,12 +129,12 @@ a -> b -> b
 
 ### Further
 
-Sometimes, writing a quick note about what type of information (like a number or text) a part of your code is expecting can be helpful. It's like leaving a little API hint for yourself and others. 
+Sometimes, writing a quick note about what type of information (like a number or text) a part of your code is expecting can be helpful. It's like leaving a little API hint for yourself and others.
 Coming back to a certain piece of code after a while you will be very thankful that you documented the APIs and don't need to rethink your entire program.
 
 When you do this, you might notice things you didn't see before.
 
-You might find out that using your code is harder than it should be. Sometimes it can help to realize why code isn't as flexible as intended. 
+You might find out that using your code is harder than it should be. Sometimes it can help to realize why code isn't as flexible as intended.
 Writing down the types helps to step back and see the big picture, making it easier to spot and fix these issues
 
 The full convention is available as mdbook [here](https://typednix.dev).

docs/book.toml

@@ -3,7 +3,7 @@ authors = ["@hsjobeki:Johannes Kirschbauer"]
 language = "en"
 multilingual = false
 src = "src"
-title = "Nix Types - first considerations"
+title = "Nix Types - Convention considerations"
 
 [output.html]
 mathjax-support = true

docs/src/SUMMARY.md

@@ -1,7 +1,6 @@
 # Summary
 
 - [Introduction](./intro.md)
-- [Getting started](./getting-started.md)
 - [Formals](./specification/formals.md)
 - [Grammar](./specification/grammar.md)
 - [Types](./specification/types.md)

docs/src/intro.md

@@ -1,53 +1,40 @@
 # Introduction
 
-This (Draft) targets the `# Type` field declared in [RFC-145](https://github.com/NixOS/rfcs/pull/145)
+This is my (draft) writing to try to formalize type convention and formals for the nix language.
+
+To support the convention utilize doc-comments.
+
+Example:
+
+````nix
+{
+  /**
+    # Type
+
+    ```
+    mapAttrs :: ( String -> a -> b ) -> { ${name} :: a; } -> { ${name} :: b; }
+    ```
+  */
+  mapAttrs = ...
+}
+````
 
 ## Motivation
 
 By specifying the syntax of the type section within nix this opens a wide range of possibilities.
 
-- consistent function / API documentation.
+- consistent function / API documentation. (I.e. used by noogle.dev)
 - Type checking - whether you call a function with the expected types.
 - Language Server (LSP) support - display inline or hover type signatures.
 - Encourage Modular architectures, with well-defined and documented interfaces.
-- Static type checking (Partial)
+- Static type / correctness checking
 
 ## Detailed implementation
 
-I propose to formulate a syntax for the `# Type` section.
-
-### No need to use code brackets
-
-using single or triple ``\` (backticks) is not necessary. The complete `# Type` section allows writing one single `type expression`. The syntax of that is specified in the following.
-
-### Builds on top of dynamic types
-
-Type information from comments can; just like in the latest js-docs; be used as a source for checking the correctness of code.
-We could imagine static type checking to work in symbiotic ways with dynamic type checking, such as YANTS (by TVL).
+I propose to formulate a strict type syntax. Be it used for doc-comments or maybe even integrated into the language itself.
 
 ### Syntax follows nix
 
 The syntax is mainly inspired and as close as possible to the Nix language. Everyone who knows Nix can easily learn the type-language for it.
 There are only very few modifications that are self-explaining and intuitive. While we could imagine a way more complex language, that allows expressing every last detailed relationship.
-We think it is more important to provide a good abstraction and find the right compromise between simplicity and expressiveness.
-
-## Comparison nixOS-modules system
-
-In general, developers must break complex parts into modules.
-Allowing them to follow the SOLID principles. Where you could write the interface definition and then develop or refactor the module behind that interface.
-As long as the interface stays the same or is downwards compatible nothing in your software breaks.
-This property is a very essential feature for writing stable and extendable code.
-
-Nix offers nixos-modules to write such modules and interface declarations. However, those declarations are boilerplate codes that may run during evaluation time.
-And also increases complexity as a lot is going on with `merge behavior` `priority (e.g. mkForce)` and so on.
-Also, it is not clear what is validated and how much it costs in terms of additional runtime overhead.
-With type annotations, this can be improved. It is not considered mutually exclusive but rather inclusive to use both worlds together.
-Validate at runtime what cannot be known statically (before runtime) and validate statically once you are sure about something in a static context. (This is essentially called a 'gradual' type system)
-A good type system would offer both and even detect automatically when to run the check.
-
-Thanks to @roberth and @theophane to point me towards this.
-
-## Future Work
-
-- In the Future, the syntax could be integrated into the Nix language. With optional typings; Just like in Python or Javascript.
-- Interface documentation could then be generated from the nix language itself if types were specified.
+I think it is more important to provide a good abstraction and find the right compromise between simplicity and expressiveness.

docs/src/nix/operations.md

@@ -35,14 +35,14 @@ The official documentation about the operators in nix can be found [here](https:
 
 ## Type signatures
 
-From a type perspective those operators can be seen as lambda functions. Every operator takes arguments of one type and returns a type.
+From a type perspective those operators can be seen as lambda functions. Every operator takes (one or more) arguments of a type and returns a type.
 The following list was created to clarify the type signatures.
 
 Some operators take one or two arguments, they can either take them from left or right hand side.
 
 ### Some formals
 
-for simplicity
+for simplicity this document follows these conventions:
 
 - `R` is used as `Right hand side` type.
 - `L` is used as `Left hand side` type.
@@ -51,23 +51,44 @@ for simplicity
 - `a`,`b`,... can be of any type. They are type variables.
 - `x` is a functions input value
 - `y` is a functions return value
+- `f`, `g`, `h` are used to give names to functions.
 
 ### '.' - Attribute selection
 
 Usage of the (`.`) operator:
 
-`L` must be an AttrSet, and `R` must evaluate to type `String`
-
-If R itself contains an expression this is parenthesized with the `${ }` operator.
-This operator tells the parser to evaluate the expression in `R` before passing it to the (`.`) function.
+`L` must be an AttrSet, and `R` must be of type `String`
 
 ```nix
- L(.)R = L.R 
+ L(.)R = L.R
 ```
 
+Since attribute sets are defined as `lists of pairs`. The `.` operation simply finds the matching `first pair` and returns the `second pair` (which is the value).
+If the value doesn't exist it raises an Error in the value world which means it returns type `Never` in the type world.
+
 ```nix
  L(.)R = L -> R -> T
- L(.)R :: { ${name} :: a } -> String -> a
+ L(.)R :: { ${name} :: a } -> String -> a | Never
+```
+
+If `R` itself contains an expression this must be parenthesized with the `( )` operator.
+This operator tells us to evaluate the expression in `R` before passing it to the (`.`) operator.
+
+Examples:
+
+```nix
+ { "car" :: String; "bus" :: Int }.("car" | "bus")
+ # Evaluates to
+ String | Int
+```
+
+#### Attribute selection in conjunction with `or`
+
+The `or` operator simply narrows out the `Never` type and instead returns a fallback value with the type of `b`.
+
+```nix
+ L.R (`or`) b = L.R or b
+ L.R (`or`) b :: { ${name} :: a } -> String -> a | b
 ```
 
 ### Function application
@@ -84,32 +105,25 @@ blow the argument `R` is applied to a function of type `L`.
 
 ```nix
  L R = L -> R -> T
- L R :: (a -> b) -> a -> b 
+ L R :: (a -> b) -> a -> b
 ```
 
 ### '-' - minus operator
 
-```nix
- y = x - 1
+```hs
+(Number -> Number -> Number)
 ```
 
-> (`-`) is a special case where the `RHS` is applied first to the function.
-> So if the `LHS` was omitted it gets the value `0` as type `Int`.
+### '+' - plus operator
 
-```nix
- L(-)R :: R -> L -> T
- (-) :: ( Int | Float ) -> ( Int | Float | 0 ) -> (Int | Float)
+```hs
+let
+Larg :: String | Path;
+Rarg  :: String | Path;
+in
+(Larg -> Rarg -> Larg) | (Number -> Number -> Number)
 ```
 
-The minus operator is a dependent type
-It depends on the received argument value
-
-- If it receives two `Int` types it returns `Int`
-- but if one or both of its arguments is of type `Float` it returns type `Float`
-- The type signature is correct using the `Number` type, but it lacks the information about its `value dependency`.
-
-### '+' - plus operator
-
 ### '?' - Has attribute
 
 ### '++' - List concatenation