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

though imo the english language text is very open to the reading that “intermarriage” would have been happening anyway

sometimes i like to point out the fact that in Japanese, DPP apparently explicitly said humans and pokémon* would intermarry in some distant past. but honestly i really like the way it was localized into english; i think the resulting text ended up being a lot more evocative, even if arguably “censored” https://legendsoflocalization.com/articles/pokemon-marrying-people/

* it also says they were indistinguishable at the time, so it might be strictly incorrect to say intermarriage was even happening

rsync CVEs, huh

the b in clodsire stands fur bifurcated

* cylinder

be careful, it does unthinkable things to your mind and ^{B O D Y}

would you smoke the blender default cylinder JUUL

mornyawn btw . also @clock, what time is it

no wonder i always liked OCaml

i said this as if OCaml weren’t a LISP in disguise

also, mornyawn . @clock, do your thing

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