Skip to content
This repository was archived by the owner on Nov 26, 2020. It is now read-only.

Add some instances #4

Merged
merged 2 commits into from
Jun 3, 2017
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
5 changes: 4 additions & 1 deletion bower.json
Original file line number Diff line number Diff line change
Expand Up @@ -15,5 +15,8 @@
"test",
"bower.json",
"package.json"
]
],
"dependencies": {
"purescript-prelude": "^3.0.0"
}
}
4 changes: 2 additions & 2 deletions package.json
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@
"build": "pulp build -- --censor-lib --strict"
},
"devDependencies": {
"pulp": "^10.0.4",
"purescript-psa": "^0.5.0-rc.1",
"pulp": "^11.0.0",
"purescript-psa": "^0.5.1",
"rimraf": "^2.6.1"
}
}
129 changes: 129 additions & 0 deletions src/Type/Proxy.purs
Original file line number Diff line number Diff line change
Expand Up @@ -48,11 +48,140 @@
-- | ```
module Type.Proxy where

import Prelude

-- | Value proxy for kind `Type` types.
data Proxy a = Proxy

derive instance eqProxy :: Eq (Proxy a)

derive instance functorProxy :: Functor Proxy

derive instance ordProxy :: Ord (Proxy a)

instance applicativeProxy :: Applicative Proxy where
pure _ = Proxy

instance applyProxy :: Apply Proxy where
apply _ _ = Proxy

instance bindProxy :: Bind Proxy where
bind _ _ = Proxy

instance booleanAlgebraProxy :: BooleanAlgebra (Proxy a)

instance boundedProxy :: Bounded (Proxy a) where
bottom = Proxy
top = Proxy

instance commutativeRingProxy :: CommutativeRing (Proxy a)

instance discardProxy :: Discard (Proxy a) where
Copy link

Choose a reason for hiding this comment

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

So this one means we'd allow discarding values of type Proxy a in do notation. Discard is meant for types like Unit so I'm not sure that's what we want.

Copy link

Choose a reason for hiding this comment

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

I mean, of course, it is a unit type, but somehow it seems to convey more information.

That said, we can't use that information in a pattern match, since we can't bind type variables, so actually I'm fine with this.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yeah, up to you whether we keep these Discard instances. I don't have enough experience with it to know if it's a good idea or a bad idea.

discard = bind

instance heytingAlgebraProxy :: HeytingAlgebra (Proxy a) where
conj _ _ = Proxy
disj _ _ = Proxy
implies _ _ = Proxy
ff = Proxy
not _ = Proxy
tt = Proxy

instance monadProxy :: Monad Proxy

instance ringProxy :: Ring (Proxy a) where
sub _ _ = Proxy

instance semigroupProxy :: Semigroup (Proxy a) where
append _ _ = Proxy

instance semiringProxy :: Semiring (Proxy a) where
add _ _ = Proxy
mul _ _ = Proxy
one = Proxy
zero = Proxy

instance showProxy :: Show (Proxy a) where
show _ = "Proxy"

-- | Value proxy for kind `Type -> Type` types.
data Proxy2 (a :: Type -> Type) = Proxy2

derive instance eqProxy2 :: Eq (Proxy2 a)

derive instance ordProxy2 :: Ord (Proxy2 a)

instance booleanAlgebraProxy2 :: BooleanAlgebra (Proxy2 a)

instance boundedProxy2 :: Bounded (Proxy2 a) where
bottom = Proxy2
top = Proxy2

instance commutativeRingProxy2 :: CommutativeRing (Proxy2 a)

instance discardProxy2 :: Discard (Proxy2 a) where
discard = bind

instance heytingAlgebraProxy2 :: HeytingAlgebra (Proxy2 a) where
conj _ _ = Proxy2
disj _ _ = Proxy2
implies _ _ = Proxy2
ff = Proxy2
not _ = Proxy2
tt = Proxy2

instance ringProxy2 :: Ring (Proxy2 a) where
sub _ _ = Proxy2

instance semigroupProxy2 :: Semigroup (Proxy2 a) where
append _ _ = Proxy2

instance semiringProxy2 :: Semiring (Proxy2 a) where
add _ _ = Proxy2
mul _ _ = Proxy2
one = Proxy2
zero = Proxy2

instance showProxy2 :: Show (Proxy2 a) where
show _ = "Proxy2"

-- | Value proxy for kind `Type -> Type -> Type` types.
data Proxy3 (a :: Type -> Type -> Type) = Proxy3

derive instance eqProxy3 :: Eq (Proxy3 a)

derive instance ordProxy3 :: Ord (Proxy3 a)

instance booleanAlgebraProxy3 :: BooleanAlgebra (Proxy3 a)

instance boundedProxy3 :: Bounded (Proxy3 a) where
bottom = Proxy3
top = Proxy3

instance commutativeRingProxy3 :: CommutativeRing (Proxy3 a)

instance discardProxy3 :: Discard (Proxy3 a) where
discard = bind

instance heytingAlgebraProxy3 :: HeytingAlgebra (Proxy3 a) where
conj _ _ = Proxy3
disj _ _ = Proxy3
implies _ _ = Proxy3
ff = Proxy3
not _ = Proxy3
tt = Proxy3

instance ringProxy3 :: Ring (Proxy3 a) where
sub _ _ = Proxy3

instance semigroupProxy3 :: Semigroup (Proxy3 a) where
append _ _ = Proxy3

instance semiringProxy3 :: Semiring (Proxy3 a) where
add _ _ = Proxy3
mul _ _ = Proxy3
one = Proxy3
zero = Proxy3

instance showProxy3 :: Show (Proxy3 a) where
show _ = "Proxy3"