Commit c6e22a3b authored by Nicolas Lenz's avatar Nicolas Lenz

Update

parent cc1336f8
# Comparisons
This compares some stuff in Haskell wtih how it could look in Katrin.
### Simple function with pattern matching
```
length :: [a] -> Int
length [] = 0
length (x:xs) = 1 + length xs
```
```
length : List a -> Nat0
[] => 0
(x::xs) => 1 + length xs
```
- DRYer
### Records
```
data Person = Person {personName :: String, personAge :: Int} -- prefixing because of name collisions
peter :: Person
peter = Person {name = "Peter", age = 65}
showName :: Person -> String
showName person = "The name is " ++ name person ++ "."
```
```
Person : Type
Name : Person -> String -- no prefixing necessary
Age : Person -> Nat0
peter : Person
Name = "Peter"
Age = 65
showName : Person -> String
person => "The name is " + person.Name + "."
```
......@@ -4,9 +4,20 @@
# I might be clinging to Haskell syntax too much. I might need to get more independent.
# No weird split between paackage name and module names like Haskell does or 1000 char long names like in Java
import "packageName.module"
Type = Set Universe // The backend of this needs a lot of thought.
// Maybe some category theory could do... something.
Nat : Type
One : Nat
Succ : Nat -> Nat
Nat0 : Type
Zero : Nat0
Succ : Nat0 -> Nat0
Maybe : Type -> Type
Nothing : Maybe a
Just : a -> Maybe a
......@@ -14,9 +25,41 @@ Maybe : Type -> Type
Pair : Type -> Type -> Type
Pair : a -> b -> Pair a b
Nat : Type
One : Nat
Succ : Nat -> Nat
List : Type -> Type
Empty : List t
Cons : t -> List t -> List t
Vector : Nat -> Type -> Type
Single : t -> Vector One t
Cons : t -> Vector n t -> Vector (Succ n) t
a : Vector 2 Nat
Single One # Type mismatch for a! Expected `Vector 2 Nat`, got `Vector 1 Nat`
b : Vector 3 Nat
1 <Cons> 2 <Cons> Single 3
c : Vector 3 Nat
[1,2,3] # Lists are overloaded
# b == c
PersonT : Type
MkPerson : String -> Int -> Person
personT : PersonT
MkPerson "Peter" 25
PersonC : Type
Name : Person -> String
Age: Person -> Int
personC : personC
Name = "Peter"
Age = 25
CoList : Type -> Type
Split : CoList a -> Maybe (a, CoList a)
isOne : Nat -> Bool
One => True
......@@ -57,7 +100,7 @@ coPlus : CoNat -> CoNat -> CoNat
x => y => case Pred y
Just y' -> {Pred = Just x} coPlus y'
ls = map (x => x *3) [List|1,2,3] # [List|3,6,9]
ls = map (x => x *3) [1,2,3] # [3,6,9]
[Set|1,2,3] == [Set|3,2,1]
......@@ -67,14 +110,7 @@ ls = map (x => x *3) [List|1,2,3] # [List|3,6,9]
f : Nat -> Nat
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))
......@@ -123,7 +159,7 @@ trait (Group a) ⇒ AbelianGroup a
# Define all those analogously, but named "Co" and with + instead of *.
# Is there a more elegant way?
# Is there a more elegant way? Named instances or something?
trait CoMagma a
_ + _ : a -> a -> a
......
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