dunhamsteve.bsky.social
Newt - a dependent typed programming language
Remove some ambiguities in parsing
+41
-39
+11
-11
playground/samples/DSL.newt
+11
-11
playground/samples/DSL.newt
···
20
20
21
21
infixr 4 _::_
22
22
data Vec : U → Nat → U where
23
-
Nil : {a} → Vec a Z
24
-
_::_ : {a k} → a → Vec a k → Vec a (S k)
23
+
Nil : ∀ a. Vec a Z
24
+
_::_ : ∀ a k. a → Vec a k → Vec a (S k)
25
25
26
26
infixl 5 _++_
27
-
_++_ : {a n m} → Vec a n → Vec a m → Vec a (n + m)
27
+
_++_ : ∀ a n m. Vec a n → Vec a m → Vec a (n + m)
28
28
Nil ++ ys = ys
29
29
(x :: xs) ++ ys = x :: (xs ++ ys)
30
30
31
-
map : {a b n} → (a → b) → Vec a n → Vec b n
31
+
map : ∀ a b n. (a → b) → Vec a n → Vec b n
32
32
map f Nil = Nil
33
33
map f (x :: xs) = f x :: map f xs
34
34
···
57
57
MkUnit : Unit
58
58
59
59
data Either : U -> U -> U where
60
-
Left : {A B} → A → Either A B
61
-
Right : {A B} → B → Either A B
60
+
Left : ∀ a b. a → Either a b
61
+
Right : ∀ a b. b → Either a b
62
62
63
63
infixr 4 _,_
64
64
data Both : U → U → U where
65
-
_,_ : {A B} → A → B → Both A B
65
+
_,_ : ∀ a b. a → b → Both a b
66
66
67
67
typ : E → U
68
68
typ Zero = Empty
···
85
85
ex1 : BothBoolBool
86
86
ex1 = (false, true)
87
87
88
-
enumAdd : {a b m n} → Vec a m → Vec b n → Vec (Either a b) (m + n)
88
+
enumAdd : ∀ a b m n. Vec a m → Vec b n → Vec (Either a b) (m + n)
89
89
enumAdd xs ys = map Left xs ++ map Right ys
90
90
91
91
-- for this I followed the shape of _*_, the lecture was slightly different
92
-
enumMul : {a b m n} → Vec a m → Vec b n → Vec (Both a b) (m * n)
92
+
enumMul : ∀ a b m n. Vec a m → Vec b n → Vec (Both a b) (m * n)
93
93
enumMul Nil ys = Nil
94
94
enumMul (x :: xs) ys = map (_,_ x) ys ++ enumMul xs ys
95
95
···
111
111
-- for now, I'll define ≡ to check
112
112
113
113
infixl 2 _≡_
114
-
data _≡_ : {A} → A → A → U where
115
-
Refl : {A} {a : A} → a ≡ a
114
+
data _≡_ : ∀ a. a → a → U where
115
+
Refl : ∀ a. {x : a} → x ≡ x
116
116
117
117
test2' : test2 ≡ false :: true :: Nil
118
118
test2' = Refl
+1
-1
playground/samples/Lists.newt
+1
-1
playground/samples/Lists.newt
···
87
87
-- same thing, but using `replace` in the proof
88
88
reverse-++-distrib' : ∀ A. (xs ys : List A) -> reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
89
89
reverse-++-distrib' Nil ys = sym (++-identity (reverse ys))
90
-
reverse-++-distrib' {A} (x :: xs) ys =
90
+
reverse-++-distrib' {a} (x :: xs) ys =
91
91
replace (\ z => (reverse (xs ++ ys) ++ (x :: Nil)) ≡ z)
92
92
(sym (++-associative (reverse ys) (reverse xs) (x :: Nil)))
93
93
(replace (\ z => (reverse (xs ++ ys)) ++ (x :: Nil) ≡ z ++ (x :: Nil)) (reverse-++-distrib' xs ys) Refl)
+8
-9
playground/samples/Tree.newt
+8
-9
playground/samples/Tree.newt
···
3
3
-- adapted from Conor McBride's 2-3 tree example
4
4
-- youtube video: https://youtu.be/v2yXrOkzt5w?t=3013
5
5
6
-
7
6
data Nat : U where
8
7
Z : Nat
9
8
S : Nat -> Nat
···
16
15
infixl 4 _+_
17
16
18
17
data _+_ : U -> U -> U where
19
-
inl : {A B} -> A -> A + B
20
-
inr : {A B} -> B -> A + B
18
+
inl : ∀ a b. a -> a + b
19
+
inr : ∀ a b. b -> a + b
21
20
22
21
infix 4 _<=_
23
22
···
47
46
_ <<= _ = Void
48
47
49
48
data Intv : Bnd -> Bnd -> U where
50
-
intv : {l u} (x : Nat) (lx : l <<= N x) (xu : N x <<= u) -> Intv l u
49
+
intv : ∀ l u. (x : Nat) (lx : l <<= N x) (xu : N x <<= u) -> Intv l u
51
50
52
51
data T23 : Bnd -> Bnd -> Nat -> U where
53
-
leaf : {l u} (lu : l <<= u) -> T23 l u Z
54
-
node2 : {l u h} (x : _)
52
+
leaf : ∀ l u. (lu : l <<= u) -> T23 l u Z
53
+
node2 : ∀ l u h. (x : _)
55
54
(tlx : T23 l (N x) h) (txu : T23 (N x) u h) ->
56
55
T23 l u (S h)
57
-
node3 : {l u h} (x y : _)
56
+
node3 : ∀ l u h. (x y : _)
58
57
(tlx : T23 l (N x) h) (txy : T23 (N x) (N y) h) (tyu : T23 (N y) u h) ->
59
58
T23 l u (S h)
60
59
···
66
65
_,_ : {A : U} {B : A -> U} -> (a : A) -> B a -> Sg A B
67
66
68
67
_*_ : U -> U -> U
69
-
A * B = Sg A (\ _ => B)
68
+
a * b = Sg a (\ _ => b)
70
69
71
70
TooBig : Bnd -> Bnd -> Nat -> U
72
71
TooBig l u h = Sg Nat (\ x => T23 l (N x) h * T23 (N x) u h)
73
72
74
-
insert : {l u h} -> Intv l u -> T23 l u h -> TooBig l u h + T23 l u h
73
+
insert : ∀ l u h. Intv l u -> T23 l u h -> TooBig l u h + T23 l u h
75
74
insert (intv x lx xu) (leaf lu) = inl (x , (leaf lx , leaf xu))
76
75
insert (intv x lx xu) (node2 y tly tyu) = case cmp x y of
77
76
-- u := N y is not solved at this time
+2
-2
playground/samples/TypeClass.newt
+2
-2
playground/samples/TypeClass.newt
···
5
5
pure : ∀ a. a → m a
6
6
7
7
infixl 1 _>>=_ _>>_
8
-
_>>=_ : {0 m} {{Monad m}} {0 a b} -> (m a) -> (a -> m b) -> m b
8
+
_>>=_ : ∀ m. {{Monad m}} {0 a b : _} -> (m a) -> (a -> m b) -> m b
9
9
ma >>= amb = bind ma amb
10
10
11
11
_>>_ : ∀ m a b. {{Monad m}} -> m a -> m b -> m b
···
15
15
Left : ∀ A B. A -> Either A B
16
16
Right : ∀ A B. B -> Either A B
17
17
18
-
instance {a} -> Monad (Either a) where
18
+
instance ∀ a. Monad (Either a) where
19
19
bind (Left a) amb = Left a
20
20
bind (Right b) amb = amb b
21
21
+1
-1
scripts/aoc25
+1
-1
scripts/aoc25
+4
-3
src/Lib/Parser.newt
+4
-3
src/Lib/Parser.newt
···
314
314
caseAlt : Parser RCaseAlt
315
315
caseAlt = do
316
316
pure MkUnit
317
-
pat <- typeExpr
317
+
pat <- term
318
318
t <- optional (keyword "=>" >> term)
319
319
pure $ MkAlt pat t
320
320
···
364
364
keyword "="
365
365
sc <- typeExpr
366
366
alts <- startBlock $ manySame $ symbol "|" *> caseAlt
367
+
-- REVIEW why am I collecting the rest here?
367
368
bodyFC <- getPos
368
369
body <- RDo <$> getPos <*> someSame doStmt
369
370
pure $ DoExpr fc (RCase fc sc Nothing (MkAlt pat (Just body) :: alts))
···
457
458
symbol "{"
458
459
quant <- quantity
459
460
names <- (some (addPos varname))
460
-
ty <- optional (symbol ":" *> typeExpr)
461
+
ty <- symbol ":" *> typeExpr
461
462
symbol "}"
462
-
pure $ map (makeBind quant ty) names
463
+
pure $ map (makeBind quant (Just ty)) names
463
464
where
464
465
makeBind : Quant → Maybe Raw → FC × String → BindInfo × Raw
465
466
makeBind quant ty (pos, name) = (BI pos name Implicit quant, fromMaybe (RImplicit pos) ty)
+7
-4
src/Prelude.newt
+7
-4
src/Prelude.newt
···
146
146
map : ∀ a b. (a → b) → m a → m b
147
147
148
148
infixr 4 _<$>_ _<$_
149
-
_<$>_ : ∀ f. {{Functor f}} {0 a b} → (a → b) → f a → f b
149
+
_<$>_ : ∀ f. {{Functor f}} {0 a b : _} → (a → b) → f a → f b
150
150
f <$> ma = map f ma
151
151
152
152
_<$_ : ∀ f a b. {{Functor f}} → b → f a → f b
···
214
214
215
215
infixr 2 _<|>_
216
216
class Alternative (m : U → U) where
217
-
_<|>_ : {0 a} → m a → m a → m a
217
+
_<|>_ : ∀ a. m a → m a → m a
218
218
219
219
instance Alternative Maybe where
220
220
Nothing <|> x = x
···
368
368
369
369
370
370
-- This is traverse, but we haven't defined Traversable yet
371
-
mapA : ∀ m. {{Applicative m}} {0 a b} → (a → m b) → List a → m (List b)
371
+
mapA : ∀ m. {{Applicative m}} {0 a b : _} → (a → m b) → List a → m (List b)
372
372
mapA f Nil = return Nil
373
373
mapA f (x :: xs) = return _::_ <*> f x <*> mapA f xs
374
374
375
375
376
-
mapM : ∀ m. {{Monad m}} {0 a b} → (a → m b) → List a → m (List b)
376
+
mapM : ∀ m. {{Monad m}} {0 a b : _} → (a → m b) → List a → m (List b)
377
377
mapM f Nil = pure Nil
378
378
mapM f (x :: xs) = do
379
379
b <- f x
···
433
433
}
434
434
`
435
435
436
+
-- FIXME this no longer works with numeric tags
437
+
-- we could take the best of both worlds and have a debug flag to add extra information
438
+
-- but also we could derive Show...
436
439
pfunc debugStr uses (natToInt listToArray) : ∀ a. a → String := `(_, obj) => {
437
440
const go = (obj) => {
438
441
if (obj === null) return "_"
+7
-8
tests/Tree.newt
+7
-8
tests/Tree.newt
···
3
3
-- adapted from Conor McBride's 2-3 tree example
4
4
-- youtube video: https://youtu.be/v2yXrOkzt5w?t=3013
5
5
6
-
7
6
data Nat : U where
8
7
Z : Nat
9
8
S : Nat -> Nat
···
16
15
infixl 4 _+_
17
16
18
17
data _+_ : U -> U -> U where
19
-
inl : {A B} -> A -> A + B
20
-
inr : {A B} -> B -> A + B
18
+
inl : ∀ a b. a -> a + b
19
+
inr : ∀ a b. b -> a + b
21
20
22
21
infix 4 _<=_
23
22
···
47
46
_ <<= _ = Void
48
47
49
48
data Intv : Bnd -> Bnd -> U where
50
-
intv : {l u} (x : Nat) (lx : l <<= N x) (xu : N x <<= u) -> Intv l u
49
+
intv : ∀ l u. (x : Nat) (lx : l <<= N x) (xu : N x <<= u) -> Intv l u
51
50
52
51
data T23 : Bnd -> Bnd -> Nat -> U where
53
-
leaf : {l u} (lu : l <<= u) -> T23 l u Z
54
-
node2 : {l u h} (x : _)
52
+
leaf : ∀ l u. (lu : l <<= u) -> T23 l u Z
53
+
node2 : ∀ l u h. (x : _)
55
54
(tlx : T23 l (N x) h) (txu : T23 (N x) u h) ->
56
55
T23 l u (S h)
57
-
node3 : {l u h} (x y : _)
56
+
node3 : ∀ l u h. (x y : _)
58
57
(tlx : T23 l (N x) h) (txy : T23 (N x) (N y) h) (tyu : T23 (N y) u h) ->
59
58
T23 l u (S h)
60
59
···
71
70
TooBig : Bnd -> Bnd -> Nat -> U
72
71
TooBig l u h = Sg Nat (\ x => T23 l (N x) h * T23 (N x) u h)
73
72
74
-
insert : {l u h} -> Intv l u -> T23 l u h -> TooBig l u h + T23 l u h
73
+
insert : ∀ l u h. Intv l u -> T23 l u h -> TooBig l u h + T23 l u h
75
74
insert (intv x lx xu) (leaf lu) = inl (x , (leaf lx , leaf xu))
76
75
insert (intv x lx xu) (node2 y tly tyu) = case cmp x y of
77
76
-- u := N y is not solved at this time