Commit c6e362d4 authored by Nicolas Lenz's avatar Nicolas Lenz

Lot of stuff, m'kay.

parent c9fd62ea
# Config file
config.yaml
# ---> Haskell
dist
dist-*
cabal-dev
*.o
*.hi
*.chi
*.chs.h
*.dyn_o
*.dyn_hi
.hpc
.hsenv
.cabal-sandbox/
cabal.sandbox.config
*.prof
*.aux
*.hp
*.eventlog
.stack-work/
cabal.project.local
.HTF/
// This file contains a wild collection examples of how Katrin code might look.
// No "module" or "package" specification. Only the file name is used.
// I might be clinging to Haskell syntax too much. I might need to get more independent.
Type = Set Universe // The backend of this needs a lot of thought.
Maybe _ : Type -> Type
Maybe a = type
Nothing : Maybe a
Just : a → Maybe a
(_,_) : Type → Type → Type // Underscore syntax shamelssly stolen from Agda. Very flexible.
(a,b) = type
(_,_) : a -> b -> (a,b)
ℕ : Type
ℕ = type
One : ℕ
Succ : ℕ → ℕ
ℤ : Type
ℤ = type
Zero : ℤ
Plus : ℕ → ℤ
Minus : ℕ → ℤ
Coℕ : Type
Coℕ = cotype
Pred : Coℕ → Maybe Coℕ
Three : ℕ
Three = Succ (Succ One)
CoTwo : Coℕ
CoTwo = {Pred = Just {Pred = Nothing}} // Provisional syntax borrowed from Haskell, I'll need to think of something better.
_ coPlus _ : Coℕ → Coℕ → Coℕ // Defining pure text functions infix should probably give a warning.
x coPlus y = case Pred y
Just y' -> {Pred = Just x} coPlus y'
// Lambda syntax ideas
f _ : ℕ → ℕ
f = x ↦ x + 10
f = λx . x + 10
f = \x . x + 10
f = \x -> x + 10
f = \x => x + 10
List _ : Type → Type
List a = type
Empty : List a
Cons : a → List a → List a
CoList _ : Type → Type
CoList a = cotype
Split : CoList a → Maybe (a, CoList a)
OneTwoThree : List Int
OneTwoThree = Cons 1 (Cons 2 (Cons 3 Empty))
CoOneTwoThree : CoList Int
CoOneTwoThree = Just (1, Just (2, (Just 3, Nothing)))
Nat : Type
Nat = ℕ
Pair _ _ : Set → Set → Set
Pair a b = type
Pair : (first : a) → (second : b) → Pair a b
// Rethink this together with the Set/Type stuff
Person : Set
Person = {Alice, Bob}
bestPair : Pair Person Person
bestPair = Pair Alice Bob
test : Set
test = {Kek, Lel, Topkek}
// Traits for algebraic structures for calculating.
trait Magma a
* : a → a → a
trait (Magma a) ⇒ Semigroup a
(x * y) * z == x * (y * z)
trait (Semigroup a) ⇒ Monoid a
1 : a
1 * x == x
x * 1 == x
trait (Monoid a) ⇒ Group a
1/ _ : a → a
trait (Group a) ⇒ AbelianGroup a
x * y == y * x
// Define all those analogously, but named "Co" and with + instead of *.
// Is there a more elegant way?
trait CoMagma a
_ + _ : a → a → a
trait (CoMagma a) ⇒ CoSemigroup a
(x + y) + z == x + (y + z)
trait (CoSemigroup a) ⇒ CoMonoid a
0 : a
0 + x == x
x + 0 == x
trait (CoMonoid a) ⇒ CoAbelianMonoid a
x + y == y + x
trait (CoMonoid a) ⇒ CoGroup a
- _ : a → a
trait (CoGroup a, CoAbelianMonoid a) ⇒ CoAbelianGroup a
trait (Monoid a, CoAbelianMonoid a) ⇒ Semiring a
x * (y + z) = (x * y) + (x * z)
(y + z) * x = (y * x) + (z * x)
trait (Semiring a, CoAbelianGroup a) ⇒ Ring a
trait (Ring a, AbelianGroup a/0) ⇒ Field a
// Probably using less mathematical and more concrete names would be a good idea.
// Instances for ℕ and ℤ. This should make normale calculations using those types possible.
instance CoMagma ℕ
x + Zero = x
x + (Succ y) = (Succ x) + y
instance CoMagma ℤ
x + Zero = x
Zero + y = y
Plus x + Plus y = x + y
Minus x + Minus y = Minus (x + y)
Plus (Succ x) + Minus One = Plus x
Plus (Succ x) + Minus (Succ y) = Plus x + Minus y
Plus One + Minus (Succ y) = Minus y
Minus x + Plus y = Plus y + Minus x
instance CoSemigroup ℕ
instance CoSemigroup ℤ
instance CoMonoid ℤ
0 = Zero
instance CoGroup ℤ
- Plus x = Minus x
- Minus x = Plus y
- Zero = Zero
instance CoAbelianGroup ℤ
instance Magma ℤ
x * Zero = Zero
x * Plus One = x
x * Plus (Succ y) = x + (x * y)
x * Minus y = - (x * Plus y)
instance Semigroup ℤ
instance Monoid ℤ
1 = Plus One
instance Ring ℤ
# Ideas for Katrin
Please note that at this point this document is just a collection of quite random notes and ideas.
Please be aware that at this point this document is just a collection of quite random notes and ideas.
## Paradigms
......@@ -25,15 +25,21 @@ Interaction (with users, windows, servers, ...) is a very important thing in pro
- Could this be used for multithreading (besides automatic parallelism of function calculations via dependencies)?
- Event-driven: Things happening on the outside are represented by events with handlers, maybe IO monads
- Look into Idris Effects
- Look into Functional Reactive Programming
- Usable as full command shell (replacing Bash etc.)
- Things like piping etc. possible with type-safety
- How to most elegantly integrate non-Katrin programs?
### Data-centric
- Communication with databases/files/servers/users should easy and type-safe
- If possible: simultaneously markup-/data-language?
- Integration with CrystalOS file/return type system
- *Languages* (regular, context-free) at the language heart
- ~~If possible: simultaneously markup-/data-language?~~
- Bad idea. Better stick to YAML as encouraged default. It can represent record types very well and is already established and less awkward to write.
- Deriving of serialization traits should be generically possible.
- Integration with CrystalOS file/return type system, one day
- ~~*Languages* (regular, context-free) at the language heart~~
- Probably nonsense
## Influenced by
......@@ -42,72 +48,32 @@ Interaction (with users, windows, servers, ...) is a very important thing in pro
- Idris
- Agda
- Python
- Go
Languages to look into: Lisp, ML, Clojure, F#, Scale, Nix, Nim
## Types
*Atom*: set of all atoms. An atom is a single part literal. Can be any string starting with a capital letter, a number and no blanks.
## Tooling
*Universe* = *Atom^\** (Kleene closure of *Atom*, i.e. any number of arbitrary atoms)
Good tooling is very important for a language.
*Type* = PowerSet(*Universe*) i.e. any subset of the universe is a type [Context free?]
One tool for everything: `katrin` command line tool is compiler, interpreter, shell, build system, formatter etc. in a single convenient place, like with Go.
*Universe**Type*!
- `katrin compile test.katrin` compiles a single file into a binary.
- `katrin shell test.katrin` starts an interactive shell with the file loaded.
- `katrin run test.katrin` or simply `katrin test.katrin` executes the file.
- `katrin build` builds a project following the directions in the `project.yaml` file.
- `katrin test` runs a KaTest test suite.
- `katrin fmt test.katrin` formats a source file following the conventions.
- `katrin lint test.katrin` gives hints on how to improve a source file.
- `katrin language-server` starts a language server for editors supporting the protocol.
```
ℕ ∈ Type
```
`→` (or `->`) takes two types and »returns« a type containing all functions from the first into the second type.
`=` defines the value of an identifier. Identifiers can be any string starting with a small letter.
**Any** string (including single character ones) denotes **either** an atom **or** an identifier.
`↦` (or `|>`) can be used to write anonymous (i.e. lambda) functions.
```
f ∈ ℕ → ℕ
f = x ↦ x*2
```
```
g ∈ ℕ → ℕ → ℕ → ℕ
g = x ↦ y ↦ z ↦ x*2 + y*4 + z*3
```
Definition of simple enum-like types:
```
oneToFour ∈ Type
oneToFour = {One, Two, Three, Four}
thing ∈ oneToFour
thing = Two
```
```
vect ∈ ℕ → Type → Type
```
Note that type names are lowercased, as they are no literals but rather identifiers for the actual type, which is a set. However, the type members (`One`, `Two`...) *are* capitalized as they are actual literals/atoms.
## Core language features
A minimal implementation would need:
- `→` and `↦` for functions
- `∈`, `=`
- Atoms, Tuples (for making literals from atoms), Sets
- pattern matching
-
- ...
Everything else should be possible to be directly implemented in the language itself (which doesn't mean that that would be the best choice performance-wise).
## Stuff
Katrin has no exceptions, functions should be total → `Maybe` return type
Katrin is by default a total language.
Lists *could* be implemented as sets of pairs of the index in the list and the actual value.
......
cabal-version: 1.12
-- This file has been generated from package.yaml by hpack version 0.31.1.
--
-- see: https://github.com/sol/hpack
--
-- hash: 3f1f9a4db7b01dd6dab03afa5875f5a4383fefec1176837dd482d66e518bcc04
name: katrin
version: 0.0.0
synopsis: Experimental functional and dependently-typet programming language
description: Please see the README at <https://git.eisfunke.com/research/katrin#readme>
category: Language
author: Nicolas Lenz
maintainer: nicolas@eisfunke.com
copyright: 2018 Nicolas Lenz
license: Apache-2.0
build-type: Simple
extra-source-files:
README.md
source-repository head
type: git
location: https://git.eisfunke.com/research/katrin
library
exposed-modules:
Katrin
Main
other-modules:
Paths_katrin
hs-source-dirs:
src
build-depends:
base >=4.7 && <5
, text
default-language: Haskell2010
executable katrin
main-is: Main.hs
other-modules:
Katrin
Paths_katrin
hs-source-dirs:
src
ghc-options: -threaded -rtsopts -with-rtsopts=-N
build-depends:
base >=4.7 && <5
, katrin
, text
default-language: Haskell2010
name: katrin
version: 0.0.0
license: Apache-2.0
git: "https://git.eisfunke.com/research/katrin"
author: "Nicolas Lenz"
maintainer: "nicolas@eisfunke.com"
copyright: "2018 Nicolas Lenz"
extra-source-files:
- README.md
synopsis: Experimental functional and dependently-typet programming language
category: Language
description: Please see the README at <https://git.eisfunke.com/research/katrin#readme>
dependencies:
- base >= 4.7 && < 5
- text
library:
source-dirs: src
executables:
katrin:
main: Main.hs
source-dirs: src
ghc-options:
- -threaded
- -rtsopts
- -with-rtsopts=-N
dependencies:
- katrin
module Katrin where
-- well.
module Main where
-- | An excellent main function.
-- | ~ Chef Excellence
main :: IO ()
main = putStrLn "Nothing to see here."
resolver: lts-12.23
packages:
- .
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment