sixten
sixten copied to clipboard
ollef
Functional programming with fewer indirections
Are you planning to support specifying erasure, e.g. like `(0 _ : x = y) -> x -> y`.
This was originally discovered in #104, and there's also a workaround there. The `ReturnDirection` pass detects when it's safe for a function that returns something of unknown type to return...
Andras Kovacs has written a nice overview of why normalisation by evaluation (NbE) is a good idea for performance [over at the Dhall Discourse](https://discourse.dhall-lang.org/t/nbe-type-checking-conversion-checking/55). I'm very fond of having well-typed...
```haskell type Tree (n : Nat) (a : Type) where Leaf : a -> Tree Zero a Fork : forall m . (Tree m a) -> (Tree m a) ->...
This currently crashes the compiler: ```haskell type Vect (n : Nat) t where Nil : forall t. Vect Zero t Cons : forall n t. t -> Vect n t...
`sixten check --watch` should use the same system for incremental compilation as the language server!
The question is how to specify what files belong to the same project. Perhaps we need a project format?
Now that there's some support for inductive families (#133), it would be cool if we could support definitions like the following: ```haskell type Vector n a where Nil : Vector...
Hackathon?
Hej! Will there be a sixten hackathon soon? I could come visit in Oslo. Cheers, Dan
We currently have the setup to test that _some_ error occurred during compilation, but we don't test that it's the correct error (other than syntax vs type error) or that...