The vague idea of a modern dependently-typed programming language.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

example.katrin 4.8KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240
  1. # This file contains a wild collection examples of how Katrin code might look.
  2. # No "module" or "package" specification. Only the file name is used.
  3. # I might be clinging to Haskell syntax too much. I might need to get more independent.
  4. # No weird split between paackage name and module names like Haskell does or 1000 char long names like in Java
  5. import "packageName.module"
  6. Type = Set Universe // The backend of this needs a lot of thought.
  7. // Maybe some category theory could do... something.
  8. Nat : Type
  9. One : Nat
  10. Succ : Nat -> Nat
  11. Nat0 : Type
  12. Zero : Nat0
  13. Succ : Nat0 -> Nat0
  14. Maybe : Type -> Type
  15. Nothing : Maybe a
  16. Just : a -> Maybe a
  17. Pair : Type -> Type -> Type
  18. Pair : a -> b -> Pair a b
  19. List : Type -> Type
  20. Empty : List t
  21. Cons : t -> List t -> List t
  22. Vector : Nat -> Type -> Type
  23. Single : t -> Vector One t
  24. Cons : t -> Vector n t -> Vector (Succ n) t
  25. a : Vector 2 Nat
  26. Single One # Type mismatch for a! Expected `Vector 2 Nat`, got `Vector 1 Nat`
  27. b : Vector 3 Nat
  28. 1 <Cons> 2 <Cons> Single 3
  29. c : Vector 3 Nat
  30. [1,2,3] # Lists are overloaded
  31. # b == c
  32. PersonT : Type
  33. MkPerson : String -> Int -> Person
  34. personT : PersonT
  35. MkPerson "Peter" 25
  36. PersonC : Type
  37. Name : Person -> String
  38. Age: Person -> Int
  39. personC : personC
  40. Name = "Peter"
  41. Age = 25
  42. CoList : Type -> Type
  43. Split : CoList a -> Maybe (a, CoList a)
  44. isOne : Nat -> Bool
  45. One => True
  46. _ => False
  47. plus' : Nat -> Nat -> Nat
  48. One => y => Succ y
  49. Succ x => y => plus' x (Succ y)
  50. syntax infix
  51. plus as +
  52. /*
  53. isOne :: Nat -> Bool
  54. isOne One = True
  55. isOne _ = False
  56. */
  57. main : Actor
  58. = new Actor
  59. input = String
  60. Integer : Type
  61. Zero : Integer
  62. Plus : Nat -> Integer
  63. Minus : Nat -> Integer
  64. CoNat : CoType
  65. Pred : CoNat -> Maybe CoNat
  66. Three : Nat = Succ (Succ One)
  67. CoTwo : CoNat = {Pred = Just {Pred = Nothing}} # Provisional record syntax borrowed from Haskell, I'll need to think of something better.
  68. coPlus : CoNat -> CoNat -> CoNat
  69. x => y => case Pred y
  70. Just y' -> {Pred = Just x} coPlus y'
  71. ls = map (x => x *3) [1,2,3] # [3,6,9]
  72. [Set|1,2,3] == [Set|3,2,1]
  73. # Lambda syntax: in1 => in2 => out
  74. # Function definition uses normal lambda syntax
  75. # Pros: One syntax rule less, less parentheses needed as the => are clear separators
  76. f : Nat -> Nat
  77. x => x + 10
  78. OneTwoThree : List Int
  79. OneTwoThree = Cons 1 (Cons 2 (Cons 3 Empty))
  80. CoOneTwoThree : CoList Int
  81. CoOneTwoThree = Just (1, Just (2, (Just 3, Nothing)))
  82. Nat : Type
  83. Nat = Nat
  84. Pair _ _ : Set -> Set -> Set
  85. Pair a b = type
  86. Pair : (first : a) -> (second : b) -> Pair a b
  87. # Rethink this together with the Set/Type stuff
  88. Person : Set
  89. Person = {Alice, Bob}
  90. bestPair : Pair Person Person
  91. bestPair = Pair Alice Bob
  92. test : Set
  93. test = {Kek, Lel, Topkek}
  94. # Traits for algebraic structures for calculating.
  95. trait Magma a
  96. * : a -> a -> a
  97. trait (Magma a) ⇒ Semigroup a
  98. (x * y) * z == x * (y * z)
  99. trait (Semigroup a) ⇒ Monoid a
  100. 1 : a
  101. 1 * x == x
  102. x * 1 == x
  103. trait (Monoid a) ⇒ Group a
  104. 1/ _ : a -> a
  105. trait (Group a) ⇒ AbelianGroup a
  106. x * y == y * x
  107. # Define all those analogously, but named "Co" and with + instead of *.
  108. # Is there a more elegant way? Named instances or something?
  109. trait CoMagma a
  110. _ + _ : a -> a -> a
  111. trait (CoMagma a) ⇒ CoSemigroup a
  112. (x + y) + z == x + (y + z)
  113. trait (CoSemigroup a) ⇒ CoMonoid a
  114. 0 : a
  115. 0 + x == x
  116. x + 0 == x
  117. trait (CoMonoid a) ⇒ CoAbelianMonoid a
  118. x + y == y + x
  119. trait (CoMonoid a) ⇒ CoGroup a
  120. - _ : a -> a
  121. trait (CoGroup a, CoAbelianMonoid a) ⇒ CoAbelianGroup a
  122. trait (Monoid a, CoAbelianMonoid a) ⇒ Semiring a
  123. x * (y + z) = (x * y) + (x * z)
  124. (y + z) * x = (y * x) + (z * x)
  125. trait (Semiring a, CoAbelianGroup a) ⇒ Ring a
  126. trait (Ring a, AbelianGroup a/0) ⇒ Field a
  127. # Probably using less mathematical and more concrete names would be a good idea.
  128. # Instances for Nat and Integer. This should make normale calculations using those types possible.
  129. instance CoMagma Nat
  130. x + Zero = x
  131. x + (Succ y) = (Succ x) + y
  132. instance CoMagma Integer
  133. x + Zero = x
  134. Zero + y = y
  135. Plus x + Plus y = x + y
  136. Minus x + Minus y = Minus (x + y)
  137. Plus (Succ x) + Minus One = Plus x
  138. Plus (Succ x) + Minus (Succ y) = Plus x + Minus y
  139. Plus One + Minus (Succ y) = Minus y
  140. Minus x + Plus y = Plus y + Minus x
  141. instance CoSemigroup Nat
  142. instance CoSemigroup Integer
  143. instance CoMonoid Integer
  144. 0 = Zero
  145. instance CoGroup Integer
  146. - Plus x = Minus x
  147. - Minus x = Plus y
  148. - Zero = Zero
  149. instance CoAbelianGroup Integer
  150. instance Magma Integer
  151. x * Zero = Zero
  152. x * Plus One = x
  153. x * Plus (Succ y) = x + (x * y)
  154. x * Minus y = - (x * Plus y)
  155. instance Semigroup Integer
  156. instance Monoid Integer
  157. 1 = Plus One
  158. instance Ring Integer