Stuff

- Explicit is better than implicit

- In general: Practical usability first, theoretical precision second

## Syntax

### Identifiers

- do-notation?

- Sensible syntax for multiline strings

## Type System

- Algebraic types

- Don't concentrate on actual types and data, but rather on "capabilities"? <http://degoes.net/articles/kill-data>

- Require explicit type signatures or not? Is it even possible to infer everything sufficiently with dependent types?

## Logic

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

    - Should be optional of course

- Error handling should be consistent

## Proofs

- Possible, but no priority – it isn't meant to be a proving tool

- [Curry-Howard correspondence](https://en.wikipedia.org/wiki/Curry–Howard_correspondence)

- How to handle trait/typeclass laws safely and usable?

## Interaction

Interaction (with users, windows, servers, ...) is a very important thing in programming. Unfortunately, it is often quite awkward (especially for beginners) in many functional languages. Find better solutions working without loads of monad transformers.

- `katrin shell` usable as full command shell (replacing bash etc.) (→ innaytool)

  - Things like piping etc. possible with type-safety

## Data Handling

In the real-world, working with external data in file systems and databases is one of the most important tasks for programs. It should be easy.

- ~~*Languages* (regular, context-free) at the language heart~~

  - *Probably* nonsense

## Interfacing

Interfacing with other languages needs to be easy. Bindings to common languages like C should be easily creatable.

Maybe a Haskell2Katrin converter for easy switching?

## Concurrency

Should be implicit in pure calculations and easilty explicitly possible for IO.

-- | Contains algebras, types and folds for Katrin abstract syntax trees.

module Katrin.AST where

{-

import Data.Text (Text)

import Data.Maybe (fromJust)

import qualified Katrin.Core as Core

    Value txt -> algebraValue txt

    Lambda txt exp -> algebraLambda txt (foldExpression alg exp)

    Subexpression exp -> algebraSubexpression (foldExpression alg exp)

-}

{-# LANGUAGE RecordWildCards #-}

-- | Contains algebras, types and folds for KatrinCore, the intermediate language for Katrin.

-- This is tightly based on the lambda calculus and the base target which is then evaluated.

-- | Contains algebras, types and folds for KatrinCore, the core language for Katrin.

-- This is currently based on the untyped λ-calculus.

module Katrin.Core where

import Data.Text (Text)

-- | Catamorphic algebraic signature for KatrinCore expressions.

data Algebra expression = Algebra {

    algebraLiteral :: Int -> expression,

    algebraValue :: Text -> expression,

    algebraBound :: Int -> expression,

    algebraFree :: Text -> expression,

    algebraApplication :: expression -> expression -> expression,

    algebraLambda :: Text -> expression -> expression

    algebraLambda :: expression -> expression

}

{-

-- | Paramorphic variant of the algebraic signature for KatrinCore.

data AlgebraPara expression = AlgebraPara {

    algebraParaLiteral :: Int -> expression,

    algebraParaValue :: Text -> expression,

    algebraParaApplication :: Expression -> expression -> Expression -> expression -> expression,

    algebraParaLambda :: Text -> Expression -> expression -> expression

-- | Converts an paramorphic algebra to an catamorphic one.

para2cata :: AlgebraPara expression -> Algebra (Expression, expression)

para2cata AlgebraPara{..} = Algebra {

    algebraLiteral = \num -> (Literal num, algebraParaLiteral num),

    algebraValue = \txt -> (Value txt, algebraParaValue txt),

    algebraApplication = \(exp1P, exp1) (exp2P, exp2) -> (Application exp1P exp2P, algebraParaApplication exp1P exp1 exp2P exp2),

    algebraLambda = \txt (expP, exp) -> (Lambda txt expP, algebraParaLambda txt expP exp)

}

-}

-- Type definition

-- | Type for lambda expressions, which are either a literal, a value identifier, a function application or a lambda function.

data Expression =

      Literal Int

    | Value Text

data Expression

    = Bound Int

    | Free Text

    | Application Expression Expression

    | Lambda Text Expression

    | Lambda Expression

    deriving (Show, Read, Eq)

data Result = Number Int | Function (Int -> Result)

-- Catamorphic fold functions

foldExpression :: Algebra expression -> Expression -> expression

foldExpression alg@Algebra{..} = \case

    (Bound index) -> algebraBound index

    (Free name) -> algebraFree name

    (Application f x) -> algebraApplication (foldExpression alg f) (foldExpression alg x)

    (Lambda exp) -> algebraLambda (foldExpression alg exp)

-- Algebras

-- | Term algebra.

algebraTerm :: Algebra Expression

algebraTerm = Algebra Literal Value Application Lambda

-- | Algebra that performs β-reduction on Katrin.

algebraBeta :: Algebra (Either Text Expression)

algebraBeta = Algebra {

    algebraLiteral = Right . Literal,

    algebraValue = Right . Value,

    algebraApplication = \exp1' exp2' -> do

        exp1 <- exp1'

        exp2 <- exp2'

        case exp1 of

            Lambda txt exp -> Right $ bind txt exp2 exp

            Value "succ" -> case exp2 of

                Literal n -> Right $ Literal $ n+1

                _ -> Right $ Application exp1 exp2

            Value txt -> Right $ Application exp1 exp2

            _ -> Left "Trying to apply something to a non-function.",

    algebraLambda = \txt exp -> exp >>= (Right . Lambda txt)

}

algebraTerm = Algebra Bound Free Application Lambda

data Value

    = ValueLambda (Value -> Value)

    | ValueNeutral Neutral

-- | Algebra for evaluating an expression.

-- This only works if the expression is completely β-reduced down to a literal.

algebraEval :: Algebra (Either Text Int)

data Neutral

    = NeutralFree Text

    | NeutralApplication Neutral Value

newtype Environment

    = Environment [Value]

algebraEval :: Algebra (Environment -> Value)

algebraEval = Algebra {

    algebraLiteral = \num -> Right num,

    algebraValue = \txt -> Left $ "Unresolved identifier " <> txt,

    algebraApplication = \exp1' exp2' -> Left "Unapplied function application",

    algebraLambda = \txt exp -> Left "Unapplied lambda"

    algebraBound = \index -> \(Environment vals) -> vals !! index,

    algebraFree = \name -> \_ -> ValueNeutral (NeutralFree name),

    algebraApplication = \f x -> \env -> apply (f env) (x env),

    algebraLambda = \exp -> \(Environment vals) -> ValueLambda (\val -> exp (Environment $ val:vals))

}

-- Catamorphic fold functions

foldExpression :: Algebra expression -> Expression -> expression

foldExpression alg@Algebra{..} = \case

    (Literal num) -> algebraLiteral num

    (Value txt) -> algebraValue txt

    (Application exp1 exp2) -> algebraApplication (foldExpression alg exp1) (foldExpression alg exp2)

    (Lambda txt exp) -> algebraLambda txt (foldExpression alg exp)

apply :: Value -> Value -> Value

apply (ValueLambda f) x = f x

apply (ValueNeutral n) x = ValueNeutral (NeutralApplication n x)

-- Helper functions

{-

-- | Replaces all values in an expression with fitting identifier with literal values

bind :: Text  -- ^ Identifier to bind

    -> Expression  -- ^ Expression to paste

    Application exp1 exp2 -> Application (bind bindId arg exp1) (bind bindId arg exp2)

    Lambda txt exp

        | txt == bindId -> Lambda txt exp

        | otherwise -> Lambda txt (bind bindId arg exp)

        | otherwise -> Lambda txt (bind bindId arg exp) -}

{-

import Text.Megaparsec.Char

import qualified Text.Megaparsec.Char.Lexer as L

-- | Main parser typedef. Parsing is done on Text without custom error component.

type Parser = Parsec Void Text

-- Lexer

-- | Comment parsers.

lineComment, blockComment :: Parser ()

lineComment = L.skipLineComment "//"

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

-- | Space consumer

sc :: Parser ()

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

sc = skipSome $ choice [skipSome $ char ' ', lineComment, blockComment]

-- | Space consumer including newlines, for between defintions

scn :: Parser ()

scn = L.space space1 lineComment blockComment

scn = L.space (skipSome $ char ' ' <|> char '\n') lineComment blockComment

lexeme :: Parser a -> Parser a

lexeme = L.lexeme sc

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

    <|> try (Literal <$> literal)

    <|> try (Value <$> identifier)

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

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