Merge

# Katrin

*Katrin* is a modern, functional, general-purpose programming language with dependent types.

*Katrin* will be a modern, functional, general-purpose programming language with dependent types.

At this point it's just [a collection of ideas](ideas.md), [some examples of future code](example.katrin) and some ground work for an algebraic compiler written in Haskell.

- ~~Mainly lazy or~~ mainly strict? (→ Haskell/Idris)

  - Probably mainly strict with explicit laziness possible (like in Idris) because of performance and algebraic typing

  - Strict evaluation -> foldr of expression tree

- Totality enforced by default (no `fromJust`, `error` etc.)?

    - Do the pros outweigh the cons here?

    - Not decidable in general, so it's a burden on the user if the totality checking fails

Katrin code ist first parsed into a normal abstract syntax tree. This is then transferred into KatrinLite, which is essentially a desugared version of Katrin. KatrinLite is then translated to KatrinCore, which is a basic representation based on the lambda calculus without any advanced features. This is then compiled to an external intermediate language which can be used with a external compiler to produce machine code.

- [Idris2](https://github.com/edwinb/Idris2) uses »quantitative type theory« as base for the core language, look into that

- [System F](https://en.wikipedia.org/wiki/System_F) (extended for GHC with GADTs to System F~c~)

- GHC uses [System F](https://en.wikipedia.org/wiki/System_F) as intermediate representation, extended with GADTs to System F~c~

- Type-checking on KatrinLite or KatrinCore?

- Optimizations on KatrinLite or KatrinCore or both? KatrinCore should be optimal for this, while some simplifications of course need to be performed when compiling Lite to Core.

- Is using two intermediate languages even helpful?

    - Idris2 also does this: They have a intermediate (TTImp) and a core language.

- Do we need a runtime system to be linked against? Probably. Look into the Haskell runtime system.

Which intermediate language could be used to produce binaries?

Which intermediate language could be used for the backend to produce binaries?

- [GraalVM](https://en.wikipedia.org/wiki/GraalVM)

    - Looks really promising

    - Supports JVM and native

    - Supports JVM and native images

    - Support for mixing with any programming language – being able to use Java, Python etc. libraries could be a *huge* advantage

- C-- (used by GHC)

    - Looks kind of obscure and doesn't really seem to be maintained.

    - Stay functional and type-safe of course

    - Maybe dependent types can be useful for this?

    - Closures?

- [Folds](https://en.wikipedia.org/wiki/Fold_(higher-order_function))

## Other Interesting Languages

### Low-Level

- [Untyped lambda calculus](https://en.wikipedia.org/wiki/Lambda_calculus) (well, duh)

    - Recursion not directly possible because of all functions being anonymous

      (That is, values can be defined and used later as syntactic sugar: `x=5; x+1` could be modelled as `(λx.x+1)5`, but this doesn't work for recursion or circular dependencies)

    - Instead it is modeled via fixed-points: [Fixed-point operator](https://en.wikipedia.org/wiki/Fixed-point_combinator)

      Instead of

      ```

      fact = λn. if n == 0 then 1 else n * fact (n-1)

      ```

      :

      ```

      fix = λg. (λx. g (x x)) (λx. g (x x))

      fact' = λr. λn. if n == 0 then 1 else n * r (n-1)

      fact = fix fact'

      ```

- [Simply-typed lambda calculus](https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus)

    - Note that this isn't turing complete as there's no recursion

    - No recursion because of impossibility to assign type to fixed-point-operator

- [System F](https://en.wikipedia.org/wiki/System_F)

- [SKI combinator calculus](https://en.wikipedia.org/wiki/SKI_combinator_calculus)

### High-Level

- Haskell

- Idris

- Agda

# Katrin Development Stages

# Katrin Roadmap

## Stage 1

## 0.1.0

Pure lambda calculus on `int`s

## Stage 2

## 0.2.0

Available features:

import qualified Katrin.Core as Core

{-|

Algebra for Katrin AST. This corresponds (is equivalent) to the context-free grammar in ABNF of Katrin:

Algebra type (signature) for Katrin AST. This corresponds (is equivalent) to the context-free grammar in ABNF of Katrin:

@

katrin = *definition

lineComment = L.skipLineComment "//"

blockComment = L.skipBlockCommentNested "/*" "*/"

-- | Space consumer

sc :: Parser ()

sc = L.space blanks lineComment blockComment where

    blanks = skipSome $ char ' '

sc = L.space (skipSome $ char ' ') lineComment blockComment

scFull :: Parser ()

scFull = L.space space1 lineComment blockComment

-- | Space consumer including newlines, for between defintions

scn :: Parser ()

scn = L.space space1 lineComment blockComment

lexeme :: Parser a -> Parser a

lexeme = L.lexeme sc

parens = between (symbol "(") (symbol ")")

literal :: Parser Int

literal = lexeme $ L.signed sc L.decimal

literal = lexeme (L.signed sc L.decimal) <?> "literal"

identifier :: Parser Text

identifier = (lexeme . try) (T.pack <$> ((:) <$> letterChar <*> many alphaNumChar))

identifier = (lexeme . try) (T.pack <$> ((:) <$> letterChar <*> many alphaNumChar)) <?> "identifier"

-- Parser

katrin :: Parser Katrin

katrin = between sc (skipMany spaceChar >> eof) (Katrin <$> definition `sepBy1` (char '\n') <?> "definition")

katrin = between scn eof (Katrin <$> definition `sepEndBy1` scn)

definition :: Parser Definition

definition = Definition <$> identifier <* symbol "=" <*> expression

segment :: Parser Segment

segment =

    try (Lambda <$> identifier <* symbol "=>" <*> expression <?> "lambda expression")

    <|> try ((Literal <$> literal) <?> "literal")

    <|> try (Value <$> identifier <?> "identifier")

    <|> try (Subexpression <$> parens expression <?> "subexpression")

    <|> try (Literal <$> literal)

    <|> try (Value <$> identifier)

    <|> try (Subexpression <$> parens expression)