dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

add list monad to tests

Browse Source
This commit is contained in:
Steve Dunham
2024-10-30 21:56:02 -07:00
parent 91eec503d1
commit a919799134
2 changed files with 81 additions and 21 deletions
Download Patch File Download Diff File Expand all files Collapse all files

50
newt/TypeClass.newt
View File

@@ -6,9 +6,15 @@ data Monad : (U -> U) -> U where
(pure : {A : U} -> A -> M A) -> (pure : {A : U} -> A -> M A) ->
Monad M Monad M
data Maybe : U -> U where infixl 1 _>>=_ _>>_
Just : {A : U} -> A -> Maybe A _>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b
Nothing : {A : U} -> Maybe A _>>=_ {a} {b} {m} {{MkMonad bind' _}} ma amb = bind' {a} {b} ma amb
_>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> m a -> m b -> m b
ma >> mb = mb
pure : {a : U} {m : U -> U} {{_ : Monad m}} -> a -> m a
pure {_} {_} {{MkMonad _ pure'}} a = pure' a
data Either : U -> U -> U where data Either : U -> U -> U where
Left : {A B : U} -> A -> Either A B Left : {A B : U} -> A -> Either A B
@@ -21,6 +27,10 @@ bindEither (Right b) amb = amb b
EitherMonad : {A : U} -> Monad (Either A) EitherMonad : {A : U} -> Monad (Either A)
EitherMonad = MkMonad {Either A} bindEither Right EitherMonad = MkMonad {Either A} bindEither Right
data Maybe : U -> U where
Just : {A : U} -> A -> Maybe A
Nothing : {A : U} -> Maybe A
bindMaybe : {A B : U} -> Maybe A -> (A -> Maybe B) -> Maybe B bindMaybe : {A B : U} -> Maybe A -> (A -> Maybe B) -> Maybe B
bindMaybe Nothing amb = Nothing bindMaybe Nothing amb = Nothing
bindMaybe (Just a) amb = amb a bindMaybe (Just a) amb = amb a
@@ -28,16 +38,30 @@ bindMaybe (Just a) amb = amb a
MaybeMonad : Monad Maybe MaybeMonad : Monad Maybe
MaybeMonad = MkMonad bindMaybe Just MaybeMonad = MkMonad bindMaybe Just
_>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b infixr 7 _::_
_>>=_ {a} {b} {m} {{MkMonad bind' _}} ma amb = bind' {a} {b} ma amb data List : U -> U where
Nil : {A : U} -> List A
_::_ : {A : U} -> A -> List A -> List A
pure : {a : U} {m : U -> U} {{_ : Monad m}} -> a -> m a infixl 7 _++_
pure {_} {_} {{MkMonad _ pure'}} a = pure' a _++_ : {A : U} -> List A -> List A -> List A
Nil ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)
infixl 1 _>>=_ _>>_ bindList : {A B : U} -> List A -> (A -> List B) -> List B
bindList Nil f = Nil
bindList (x :: xs) f = f x ++ bindList xs f
_>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> m a -> m b -> m b singleton : {A : U} -> A -> List A
ma >> mb = mb singleton a = a :: Nil
-- TODO need better error when the monad is not defined
ListMonad : Monad List
ListMonad = MkMonad bindList singleton
infixr 1 _,_
data Pair : U -> U -> U where
_,_ : {A B : U} -> A -> B -> Pair A B
ptype Int ptype Int
@@ -52,3 +76,9 @@ bar x = do
let y = x let y = x
z <- Just x z <- Just x
pure z pure z
baz : {A B : U} -> List A -> List B -> List (Pair A B)
baz xs ys = do
x <- xs
y <- ys
pure (x , y)

52
tests/black/TypeClass.newt
View File

@@ -6,9 +6,15 @@ data Monad : (U -> U) -> U where
(pure : {A : U} -> A -> M A) -> (pure : {A : U} -> A -> M A) ->
Monad M Monad M
data Maybe : U -> U where infixl 1 _>>=_ _>>_
Just : {A : U} -> A -> Maybe A _>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b
Nothing : {A : U} -> Maybe A _>>=_ {a} {b} {m} {{MkMonad bind' _}} ma amb = bind' {a} {b} ma amb
_>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> m a -> m b -> m b
ma >> mb = mb
pure : {a : U} {m : U -> U} {{_ : Monad m}} -> a -> m a
pure {_} {_} {{MkMonad _ pure'}} a = pure' a
data Either : U -> U -> U where data Either : U -> U -> U where
Left : {A B : U} -> A -> Either A B Left : {A B : U} -> A -> Either A B
@@ -21,6 +27,10 @@ bindEither (Right b) amb = amb b
EitherMonad : {A : U} -> Monad (Either A) EitherMonad : {A : U} -> Monad (Either A)
EitherMonad = MkMonad {Either A} bindEither Right EitherMonad = MkMonad {Either A} bindEither Right
data Maybe : U -> U where
Just : {A : U} -> A -> Maybe A
Nothing : {A : U} -> Maybe A
bindMaybe : {A B : U} -> Maybe A -> (A -> Maybe B) -> Maybe B bindMaybe : {A B : U} -> Maybe A -> (A -> Maybe B) -> Maybe B
bindMaybe Nothing amb = Nothing bindMaybe Nothing amb = Nothing
bindMaybe (Just a) amb = amb a bindMaybe (Just a) amb = amb a
@@ -28,16 +38,30 @@ bindMaybe (Just a) amb = amb a
MaybeMonad : Monad Maybe MaybeMonad : Monad Maybe
MaybeMonad = MkMonad bindMaybe Just MaybeMonad = MkMonad bindMaybe Just
_>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b infixr 7 _::_
_>>=_ {a} {b} {m} {{MkMonad bind' _}} ma amb = bind' {a} {b} ma amb data List : U -> U where
Nil : {A : U} -> List A
_::_ : {A : U} -> A -> List A -> List A
pure : {a : U} {m : U -> U} {{_ : Monad m}} -> a -> m a infixl 7 _++_
pure {_} {_} {{MkMonad _ pure'}} a = pure' a _++_ : {A : U} -> List A -> List A -> List A
Nil ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)
infixl 1 _>>=_ _>>_ bindList : {A B : U} -> List A -> (A -> List B) -> List B
bindList Nil f = Nil
bindList (x :: xs) f = f x ++ bindList xs f
_>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> m a -> m b -> m b singleton : {A : U} -> A -> List A
ma >> mb = mb singleton a = a :: Nil
-- TODO need better error when the monad is not defined
ListMonad : Monad List
ListMonad = MkMonad bindList singleton
infixr 1 _,_
data Pair : U -> U -> U where
_,_ : {A B : U} -> A -> B -> Pair A B
ptype Int ptype Int
@@ -45,10 +69,16 @@ test : Maybe Int
test = pure 10 test = pure 10
foo : Int -> Maybe Int foo : Int -> Maybe Int
foo x = Just 42 >> Just x >>= (\ x => pure 10) foo x = Just 42 >> Just x >>= (\ x => pure {_} {Maybe} 10)
bar : Int -> Maybe Int bar : Int -> Maybe Int
bar x = do bar x = do
let y = x let y = x
z <- Just x z <- Just x
pure z pure z
baz : {A B : U} -> List A -> List B -> List (Pair A B)
baz xs ys = do
x <- xs
y <- ys
pure (x , y)