forall / ∀ syntactic sugar

TODO.md

@@ -1,7 +1,7 @@
 
 ## TODO
 
-- [ ] forall / ∀ sugar
+- [x] forall / ∀ sugar
 - [ ] Bad module name error has FC 0,0 instead of the module or name
 - [x] I've made `{x}` be `{x : _}` instead of `{_ : x}`. Change this.
 - [ ] Remove context lambdas when printing solutions (show names from context)

newt-vscode/syntaxes/newt.tmLanguage.json

@@ -16,7 +16,7 @@
     },
     {
       "name": "keyword.newt",
-      "match": "\\b(data|where|case|of|let|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b"
+      "match": "\\b(data|where|case|of|let|forall|∀|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b"
     },
     {
       "name": "string.js",

playground/samples/Lists.newt

@@ -21,17 +21,17 @@ S n + m = S (n + m)
 -- A list is empty (Nil) or a value followed by a list (separated by the :: operator)
 infixr 3 _::_
 data List : U -> U where
-    Nil : {A : U} -> List A
+    Nil : ∀ A. List A
-    _::_ : {A : U} -> A -> List A -> List A
+    _::_ : ∀ A. A -> List A -> List A
 
 -- length of a list is defined inductively
-length : {A : U} -> List A -> Nat
+length : ∀ A . List A -> Nat
 length Nil = Z
 length (x :: xs) = S (length xs)
 
 -- List concatenation
 infixl 2 _++_
-_++_ : {A : U} -> List A -> List A -> List A
+_++_ : ∀ A. List A -> List A -> List A
 Nil ++ ys = ys
 x :: xs ++ ys = x :: (xs ++ ys)
 
@@ -40,8 +40,8 @@ x :: xs ++ ys = x :: (xs ++ ys)
 -- Magic happens in the compiler when it tries to make the types
 -- fit into this.
 infixl 1 _≡_
-data _≡_ : {A : U} -> A -> A -> U where
+data _≡_ : ∀ A . A -> A -> U where
-    Refl : {A : U} {a : A} -> a ≡ a
+    Refl : ∀ A . {a : A} -> a ≡ a
 
 -- If a ≡ b then b ≡ a
 sym : {A : U} {a b : A} -> a ≡ b -> b ≡ a
@@ -60,32 +60,32 @@ cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
 
 -- if concatenate two lists, the length is the sum of the lengths
 -- of the original lists
-length-++ : {A : U} (xs ys : List A) -> length (xs ++ ys) ≡ length xs + length ys
+length-++ : ∀ A. (xs ys : List A) -> length (xs ++ ys) ≡ length xs + length ys
 length-++ Nil ys = Refl
 length-++ (x :: xs) ys = cong S (length-++ xs ys)
 
 -- a function to reverse a list
-reverse : {A : U} -> List A -> List A
+reverse : ∀ A. List A -> List A
 reverse Nil = Nil
 reverse (x :: xs) = reverse xs ++ (x :: Nil)
 
 -- if we add an empty list to a list, we get the original back
-++-identity : {A : U} -> (xs : List A) -> xs ++ Nil ≡ xs
+++-identity : ∀ A. (xs : List A) -> xs ++ Nil ≡ xs
 ++-identity Nil = Refl
 ++-identity (x :: xs) = cong (_::_ x) (++-identity xs)
 
 -- concatenation is associative
-++-associative : {A : U} (xs ys zs : List A) -> xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
+++-associative : ∀ A. (xs ys zs : List A) -> xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
 
 -- reverse distributes over ++, but switches order
-reverse-++-distrib : {A : U} -> (xs ys : List A) -> reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
+reverse-++-distrib : ∀ A. (xs ys : List A) -> reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
 reverse-++-distrib Nil ys = sym (++-identity (reverse ys))
 reverse-++-distrib (x :: xs) ys =
   trans (cong (\ z => z ++ (x :: Nil)) (reverse-++-distrib xs ys))
         (sym (++-associative (reverse ys) (reverse xs) (x :: Nil)))
 
 -- same thing, but using `replace` in the proof
-reverse-++-distrib' : {A : U} -> (xs ys : List A) -> reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
+reverse-++-distrib' : ∀ A. (xs ys : List A) -> reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
 reverse-++-distrib' Nil ys = sym (++-identity (reverse ys))
 reverse-++-distrib' {A} (x :: xs) ys =
   replace (\ z => (reverse (xs ++ ys) ++ (x :: Nil)) ≡ z)
@@ -93,28 +93,28 @@ reverse-++-distrib' {A} (x :: xs) ys =
           (replace (\ z => (reverse (xs ++ ys)) ++ (x :: Nil) ≡ z ++ (x :: Nil)) (reverse-++-distrib' xs ys) Refl)
 
 -- reverse of reverse gives you the original list
-reverse-involutive : {A : U} -> (xs : List A) -> reverse (reverse xs) ≡ xs
+reverse-involutive : ∀ A. (xs : List A) -> reverse (reverse xs) ≡ xs
 reverse-involutive Nil = Refl
 reverse-involutive (x :: xs) =
   trans (reverse-++-distrib (reverse xs) (x :: Nil))
         (cong (_::_ x) (reverse-involutive xs))
 
 -- helper for a different version of reverse
-shunt : {A : U} -> List A -> List A -> List A
+shunt : ∀ A. List A -> List A -> List A
 shunt Nil ys = ys
 shunt (x :: xs) ys = shunt xs (x :: ys)
 
 -- lemma
-shunt-reverse : {A : U} (xs ys : List A) -> shunt xs ys ≡ reverse xs ++ ys
+shunt-reverse : ∀ A. (xs ys : List A) -> shunt xs ys ≡ reverse xs ++ ys
 shunt-reverse Nil ys = Refl
 shunt-reverse (x :: xs) ys =
   trans (shunt-reverse xs (x :: ys))
         (++-associative (reverse xs) (x :: Nil) ys)
 
 -- an alternative definition of reverse
-reverse' : {A : U} -> List A -> List A
+reverse' : ∀ A. List A -> List A
 reverse' xs = shunt xs Nil
 
 -- proof that the reverse and reverse' give the same results
-reverses : {A : U} → (xs : List A) → reverse' xs ≡ reverse xs
+reverses : ∀ A. (xs : List A) → reverse' xs ≡ reverse xs
 reverses xs = trans (shunt-reverse xs Nil) (++-identity _)

playground/samples/Tour.newt

@@ -77,13 +77,13 @@ test = Refl
 infixl 7 _+_
 
 -- We don't have records yet, so we define a single constructor
--- inductive type:
+-- inductive type. Here we also use `∀ A.` which is sugar for `{A : _} ->`
 data Plus : U -> U where
-  MkPlus : {A : U} -> (A -> A -> A) -> Plus A
+  MkPlus : ∀ A. (A -> A -> A) -> Plus A
 
 -- and the generic function that uses it
 -- the double brackets indicate an argument that is solved by search
-_+_ : {A : U} {{_ : Plus A}} -> A -> A -> A
+_+_ : ∀ A. {{_ : Plus A}} -> A -> A -> A
 _+_ {{MkPlus f}} x y = f x y
 
 -- The typeclass is now defined, search will look for functions in scope
@@ -150,31 +150,31 @@ data Monad : (U -> U) -> U where
             ({a b : U} -> m a -> (a -> m b) -> m b) ->
             Monad m
 
-pure : {m : U -> U} -> {{_ : Monad m}} -> {a : U} -> a -> m a
+pure : ∀ m . {{_ : Monad m}} -> {a : U} -> a -> m a
 pure {{MkMonad p _}} a = p a
 
 -- we can declare multiple infix operators at once
 infixl 1 _>>=_ _>>_
 
-_>>=_ : {m : U -> U} -> {{_ : Monad m}} -> {a b : U} -> m a -> (a -> m b) -> m b
+_>>=_ : ∀ m a b. {{_ : Monad m}} -> m a -> (a -> m b) -> m b
 _>>=_ {{MkMonad _ b}} ma amb = b ma amb
 
-_>>_ :  {m : U -> U} -> {{_ : Monad m}} -> {a b : U} -> m a -> m b -> m b
+_>>_ :  ∀ m a b. {{_ : Monad m}} -> m a -> m b -> m b
 ma >> mb = ma >>= (λ _ => mb)
 
 -- That's our Monad typeclass, now let's make a List monad
 
 infixr 3 _::_
 data List : U -> U where
-  Nil : {A : U} -> List A
+  Nil : ∀ A.  List A
-  _::_ : {A : U} -> A -> List A -> List A
+  _::_ : ∀ A. A -> List A -> List A
 
 infixr 7 _++_
-_++_ : {a : U} -> List a -> List a -> List a
+_++_ : ∀ a.  List a -> List a -> List a
 Nil ++ ys = ys
 (x :: xs) ++ ys = x :: (xs ++ ys)
 
-bindList : {a b : U} -> List a -> (a -> List b) -> List b
+bindList : ∀ a b. List a -> (a -> List b) -> List b
 bindList Nil f = Nil
 bindList (x :: xs) f = f x ++ bindList xs f
 
@@ -186,11 +186,11 @@ MonadList = MkMonad (λ a => a :: Nil) bindList
 -- Also we see that → can be used in lieu of ->
 infixr 1 _,_ _×_
 data _×_ : U → U → U where
-  _,_ : {A B : U} → A → B → A × B
+  _,_ : ∀ A B. A → B → A × B
 
 -- The _>>=_ operator is used for desugaring do blocks
 
-prod : {A B : U} → List A → List B → List (A × B)
+prod : ∀ A B. List A → List B → List (A × B)
 prod xs ys = do
   x <- xs
   y <- ys

playground/src/monarch.ts

@@ -70,6 +70,8 @@ export let newtTokens: monaco.languages.IMonarchLanguage = {
     "case",
     "of",
     "data",
+    "forall",
+    "∀",
     "U",
     "module",
     "ptype",

src/Lib/Parser.idr

@@ -252,6 +252,15 @@ arrow : Parser Unit
 arrow = sym "->" <|> sym "→"
 
 -- Collect a bunch of binders (A : U) {y : A} -> ...
+
+forAll : Parser Raw
+forAll = do
+  keyword "forall" <|> keyword "∀"
+  all <- some (withPos varname)
+  keyword "."
+  scope <- typeExpr
+  pure $ foldr (\ (fc, n), sc => RPi fc (Just n) Implicit (RImplicit fc) sc) scope all
+
 binders : Parser Raw
 binders = do
   binds <- many (abind <|> ibind <|> ebind)
@@ -262,7 +271,9 @@ binders = do
     mkBind : FC -> (String, Icit, Raw) -> Raw -> Raw
     mkBind fc (name, icit, ty) scope = RPi fc (Just name) icit ty scope
 
-typeExpr = binders
+typeExpr
+  = binders
+  <|> forAll
   <|> do
         fc <- getPos
         exp <- term

src/Lib/Tokenizer.idr

@@ -8,10 +8,8 @@ import Lib.Common
 keywords : List String
 keywords = ["let", "in", "where", "case", "of", "data", "U", "do",
             "ptype", "pfunc", "module", "infixl", "infixr", "infix",
-            "->", "→", ":", "=>", ":=", "=", "<-", "\\", "_"]
+            "∀", "forall", ".",
-
+             "->", "→", ":", "=>", ":=", "=", "<-", "\\", "_"]
-specialOps : List String
-specialOps = ["->", ":", "=>", ":=", "=", "<-"]
 
 checkKW : String -> Token Kind
 checkKW s = if elem s keywords then Tok Keyword s else Tok Ident s
@@ -20,10 +18,10 @@ checkUKW : String -> Token Kind
 checkUKW s = if elem s keywords then Tok Keyword s else Tok UIdent s
 
 identMore : Lexer
-identMore = alphaNum <|> exact "." <|> exact "'" <|> exact "_"
+identMore = alphaNum <|> exact "'" <|> exact "_"
 
 singleton : Lexer
-singleton = oneOf "()\\{}[],?"
+singleton = oneOf "()\\{}[],?."
 
 quo : Recognise True
 quo = is '"'