vyorkin/purescript-unicode-prelude

Add "existential" Data.Array operators

vyorkin opened this issue · 2 comments

vyorkin commented

In Haskell we have separate container-unicode-symbols package that

defines new symbols for a number of functions and operators in the containers package

But in PureScript instead of one containers package we have several packages like purescript-foldable-traversable, purescript-arrays, etc.

So I'm not really sure where this should be:

module Data.Foldable.Unicode
  ( thereExists
  , forAll
  , (∀)
  , (∃)
  ) where

import Data.Foldable (class Foldable, all, any)
import Prelude (class HeytingAlgebra, flip)

thereExists ∷ ∀ a f h e. Foldable f ⇒ HeytingAlgebra h ⇒ a → f e → (e → h) → h
thereExists _ elements predicate = any predicate elements

-- | (∃) = ('∃')
-- | U+2203, THERE EXIST OPERATOR
-- |
-- | Usage:
-- | ```purescript
-- |  __ ∃ [1, -3] : (_ > 0) -- ≡ true
-- | ```
infixl 10 thereExists as ∃

forAll ∷ ∀ a f h e. Foldable f ⇒ HeytingAlgebra h ⇒ a → f e → (e → h) → h
forAll _ = flip all

-- | (∀) = ('∀')
-- | U+2200, FOR ALL OPERATOR
-- |
-- | Usage:
-- | ```purescript
-- | __ ∀ [1, -3] : (_ > 0) -- ≡ false
-- | ```
infixr 10 forAll as ∀
csicar commented

Might just delete it. It really wasn't hat useful.
After all it required placing a dummy Argument __ in Front of forall making it quite annoying to use.

  • 👍1