Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add Applicative trait #115

Merged
merged 8 commits into from
Aug 21, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ html:
PHONY: clean
clean:
rm -rf docs
$(MAKE) -C test/ clean

.PHONY: test
test:
Expand Down
11 changes: 10 additions & 1 deletion Stdlib/Data/List.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ import Stdlib.Function open;
import Stdlib.Trait.Eq open;
import Stdlib.Trait.Ord open;
import Stdlib.Trait.Show open;
import Stdlib.Trait.Functor open;
import Stdlib.Trait open;
import Stdlib.Trait.Partial open;
Comment on lines -11 to 12
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you use import Stdlib.Trait open are the other Trait imports redundant?

import Stdlib.Trait.Foldable open using {Foldable; module Polymorphic; fromPolymorphicFoldable};

Expand Down Expand Up @@ -75,3 +75,12 @@ polymorphicFoldableListI : Polymorphic.Foldable List :=
{-# specialize: true, inline: true #-}
instance
foldableListI {A} : Foldable (List A) A := fromPolymorphicFoldable;

instance
applicativeListI : Applicative List :=
mkApplicative@{
pure {A} (a : A) : List A := [a];
ap {A B} : List (A -> B) -> List A -> List B
| [] _ := []
| (f :: fs) l := map f l ++ ap fs l
};
10 changes: 10 additions & 0 deletions Stdlib/Data/Maybe.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ import Stdlib.Trait.Eq open;
import Stdlib.Trait.Ord open;
import Stdlib.Trait.Show open;
import Stdlib.Trait.Functor open;
import Stdlib.Trait.Applicative open;

import Stdlib.Data.Bool.Base open;
import Stdlib.Data.String.Base open;
Expand Down Expand Up @@ -51,3 +52,12 @@ functorMaybeI : Functor Maybe :=
{-# specizalize: true, inline: true #-}
instance
monomorphicFunctorMaybeI {A} : Monomorphic.Functor (Maybe A) A := fromPolymorphicFunctor;

instance
applicativeMaybeI : Applicative Maybe :=
mkApplicative@{
pure := just;
ap {A B} : Maybe (A -> B) -> Maybe A -> Maybe B
| (just f) (just x) := just (f x)
| _ _ := nothing
};
12 changes: 11 additions & 1 deletion Stdlib/Data/Result.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ import Stdlib.Data.Bool.Base open;

import Stdlib.Trait.Eq open;
import Stdlib.Trait.Ord open;
import Stdlib.Trait.Functor open;
import Stdlib.Trait open;
Comment on lines 7 to +8
Copy link
Collaborator

@paulcadman paulcadman Aug 5, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you use import Stdlib.Trait open are the other Trait imports redundant?


{-# specialize: true, inline: case #-}
instance
Expand Down Expand Up @@ -39,3 +39,13 @@ functorResultI {err} : Functor (Result err) :=
instance
monomorphicFunctorResultI {err res} : Monomorphic.Functor (Result err res) res :=
fromPolymorphicFunctor;

instance
applicativeResultI {err} : Applicative (Result err) :=
mkApplicative@{
pure := ok;
ap {A B} : Result err (A -> B) -> Result err A -> Result err B
| (ok f) (ok x) := ok (f x)
| (ok _) (error e) := error e
| (error e) _ := error e
};
5 changes: 1 addition & 4 deletions Stdlib/Data/Unit.juvix
Original file line number Diff line number Diff line change
@@ -1,17 +1,14 @@
--- The unit type.
module Stdlib.Data.Unit;

import Stdlib.Data.Unit.Base open public;
import Stdlib.Data.Bool.Base open;

import Stdlib.Trait.Eq open;
import Stdlib.Trait.Ord open;
import Stdlib.Trait.Show open;
import Stdlib.Trait.Foldable open;

type Unit :=
--- The only constructor of ;Unit;.
unit;

instance
eqUnitI : Eq Unit := mkEq λ {unit unit := true};

Expand Down
13 changes: 13 additions & 0 deletions Stdlib/Data/Unit/Base.juvix
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
--- The unit type.
module Stdlib.Data.Unit.Base;

import Stdlib.Data.Bool.Base open;

import Stdlib.Trait.Eq open;
import Stdlib.Trait.Ord open;
import Stdlib.Trait.Show open;
import Stdlib.Trait.Foldable open;

type Unit :=
--- The only constructor of ;Unit;.
unit;
1 change: 1 addition & 0 deletions Stdlib/Trait.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ import Stdlib.Trait.Eq as Eq open using {Eq; module Eq} public;
import Stdlib.Trait.Show as Show open using {Show; module Show} public;
import Stdlib.Trait.Ord as Ord open using {Ord; module Ord} public;
import Stdlib.Trait.Functor open public;
import Stdlib.Trait.Applicative open public;
import Stdlib.Trait.Foldable open public;
import Stdlib.Trait.Partial open public;
import Stdlib.Trait.Natural open public;
Expand Down
49 changes: 49 additions & 0 deletions Stdlib/Trait/Applicative.juvix
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
module Stdlib.Trait.Applicative;

import Stdlib.Data.Fixity open;
import Stdlib.Function open;
import Stdlib.Data.Bool.Base open;
import Stdlib.Data.Nat.Base open;
import Stdlib.Data.List.Base open;
import Stdlib.Data.Unit.Base open;
import Stdlib.Trait.Functor open;
import Stdlib.Trait.Foldable.Polymorphic open;
import Stdlib.Data.Unit.Base open;

trait
type Applicative (f : Type -> Type) :=
mkApplicative {
{{functor}} : Functor f;
pure : {A : Type} -> A -> f A;
ap : {A B : Type} -> f (A -> B) -> f A -> f B
};

open Applicative public;

--- Sequences computations.
--- Note that this function will be renamed to >>> once IO becomses a polymorphic type and can be given an Applicative instance.
applicativeSeq {f : Type -> Type} {{Applicative f}} {A B : Type} (fa : f A) (fb : f B) : f B :=
ap (map λ {_ b := b} fa) fb;

--- lifts a binary function to ;Applicative;
liftA2 {f : Type -> Type} {{Applicative f}} {A B C} (fun : A -> B -> C) : f A -> f B -> f C :=
map fun >> ap;

syntax iterator mapA_ {init := 0; range := 1};
mapA_
{t : Type -> Type}
{f : Type -> Type}
{A B}
{{Foldable t}}
{{Applicative f}}
(fun : A -> f B)
(l : t A)
: f Unit := rfor (acc := pure unit) (x in l) {applicativeSeq (fun x) acc};

replicateA {f : Type -> Type} {A} {{Applicative f}} : Nat -> f A -> f (List A)
| zero _ := pure []
| (suc n) x := liftA2 (::) x (replicateA n x);

when {f : Type -> Type} {{Applicative f}} : Bool -> f Unit -> f Unit
| false _ := pure unit
| true a := a;
2 changes: 1 addition & 1 deletion test/Package.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -6,5 +6,5 @@ package : Package :=
defaultPackage@?{
name := "stdlib-test";
dependencies :=
[path "../"; github "anoma" "juvix-quickcheck" "eca0d109869eeb7b708162634f4917f270139da1"]
[path "../"; github "anoma" "juvix-quickcheck" "104c749950480ed5dad42c7385a020ff31ca8875"]
};
8 changes: 4 additions & 4 deletions test/juvix.lock.yaml
Original file line number Diff line number Diff line change
@@ -1,18 +1,18 @@
# This file was autogenerated by Juvix version 0.6.4.
# This file was autogenerated by Juvix version 0.6.5.
# Do not edit this file manually.

version: 2
checksum: fe279cadfedcac3f17d3557f5b1bbc168a153b29b6876bd56df33e21aad59ee5
checksum: 74c7b4f7ff78859f15da9fa14ede6df5397c698d1efdcd5cc0f435d5cbb59e9d
dependencies:
- path: ../
dependencies: []
- git:
name: anoma_juvix-quickcheck
ref: eca0d109869eeb7b708162634f4917f270139da1
ref: 104c749950480ed5dad42c7385a020ff31ca8875
url: https://github.com/anoma/juvix-quickcheck
dependencies:
- git:
name: anoma_juvix-stdlib
ref: 297601a98dcace657aaff6e42945f1430647885b
ref: 0ca2d5181e7c98eceace5c12bfd0a8cfb3d4d132
url: https://github.com/anoma/juvix-stdlib
dependencies: []
Loading