Define Sieve and Cosieve interfaces

This commit is contained in:
Kiana Sheibani 2023-03-06 21:37:27 -05:00
parent 22da62a6f5
commit ff82a24001
Signed by: toki
GPG key ID: 6CB106C25E86A9F7

View file

@ -0,0 +1,15 @@
module Data.Profunctor.Sieve
import Data.Profunctor
%default total
public export
interface (Profunctor p, Functor f) => Sieve p f | p where
sieve : p a b -> a -> f b
public export
interface (Profunctor p, Functor f) => Cosieve p f | p where
cosieve : p a b -> f a -> b