æʃliŋ, loaf of autismo @aescling@cat.family

@vaporeon_ this is hard to expurress succinctly.

(C t) => ... means that in the type expurression ..., the type t is known to be a member of the typeclass C

an example of a typeclass is Eq, fur types that have total equality checks:

class Eq a where
  (==) :: a -> a -> Bool
  (/=) :: a -> a -> Bool

so, fur example, the following (extremely trivial) function, we contrain the polymorphism of f to parameterize only on types which are known instances of Eq, making it legal to polymorphically invoke the equality check on the generic parameter a:

f :: Eq t => t -> Bool
f a = a == a

@vaporeon_ i WROTE this code and i am struggling to purrocess it

filtering ::
  (Applicative k) =>
  (a -> k Bool) ->
  List a ->
  k (List a)
filtering p = foldRight g $ pure Nil
  where
    -- what the fuck even is this
    g a as = f a <$> p a <*> as

    f :: a -> Bool -> List a -> List a
    f _ False as = as
    f a True as = a :. as

structural recursion my beloved. still don't understand this though

the thing about following the types and using the compiler to find the types of your holes is that, while it will create code that compiles and apparently passes the tests, it will also create code that is inscrutable to YOU

-- | Filter a list with a predicate that produces an effect.
--
-- >>> filtering (ExactlyOne . even) (4 :. 5 :. 6 :. Nil)
-- ExactlyOne [4,6]
--
-- >>> filtering (\a -> if a > 13 then Empty else Full (a <= 7)) (4 :. 5 :. 6 :. Nil)
-- Full [4,5,6]
--
-- >>> filtering (\a -> if a > 13 then Empty else Full (a <= 7)) (4 :. 5 :. 6 :. 7 :. 8 :. 9 :. Nil)
-- Full [4,5,6,7]
--
-- >>> filtering (\a -> if a > 13 then Empty else Full (a <= 7)) (4 :. 5 :. 6 :. 13 :. 14 :. Nil)
-- Empty
--
-- >>> filtering (>) (4 :. 5 :. 6 :. 7 :. 8 :. 9 :. 10 :. 11 :. 12 :. Nil) 8
-- [9,10,11,12]
--
-- >>> filtering (const $ True :. True :.  Nil) (1 :. 2 :. 3 :. Nil)
-- [[1,2,3],[1,2,3],[1,2,3],[1,2,3],[1,2,3],[1,2,3],[1,2,3],[1,2,3]]
filtering ::
  (Applicative k) =>
  (a -> k Bool) ->
  List a ->
  k (List a)
filtering _ Nil = pure Nil
-- what the fuck even is this
filtering p (k :. ks) = f k <$> p k <*> filtering p ks
  where
    f :: a -> Bool -> List a -> List a
    f _ False as = as
    f a True as = a :. as

-- what the fuck even is this

the calculus of inductive constructions would be an acceptable alternative i guess

i guess the closest is the toy language used in The Little Typer

even though the pi calculus is decidedly not hindley-milner

i wish there were a strictly typed LISP using a hindley-milner type system

@The_T @wallhackio @vaporeon_ i don’t like trying to remember that period of time fur myself

(from https://blacksky.community/profile/did:plc:5ysft3tkkncrn3xohxwqybxl/post/3mm4x4psvrs2f)

@coriander he’s purrfect

ny’all, including you, @clock

@compufox here have a DIFFURENT earworm >:3 https://www.youtube.com/watch?v=4PyFkH9LCGQ

@wallhackio i agree with the subject line