Matúš Tejiščák

Unchecked vector access

1

Here's a program reading out of bounds: ```bash $ echo '(module (_ (load.byte "" 1)) (export))' > example.mlf $ malfunction compile example.mlf -o example ``` The program compiles fine. Then...

If I change the implementation of module `X` but not its interface, it would be nice to not have to recompile all modules (transitively) depending on `X`. With `ocamlopt`, this...

The `Maybe` hack means that `Just x` compiles to `x` and `Nothing` compiles to `None`. If there's a value `v` that compiles to `None`, such as `Nothing`, then `Just v`...

RFC: Generalised dot syntax for postfix application

5

Here's a more radical idea: `.(expr) and .name` are postfix applications of `expr`/`name` that bind tighter than application. Some examples: * `printLn user.name.length` * `"hello".length.(+3).printLn` * `map (.length.show) ["foo", "booo"]`...

# Steps to Reproduce ```idris import Data.Vect %default total data Number = N1 | N2 | N3 | N4 Eq Number where N1 == N1 = True N2 == N2...

Incorrect reduction of pattern matching

4

# Steps to Reproduce ```idris import Data.Vect %default total infix 3 . Bool (. True _ => False countGreater : (thr : Int) -> (ctx : Vect n Int) ->...