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

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

this aged very depurressingly

It has been pointed out again and again that the practical potential of computational linguistics, and of computational semantics as an essential part of it, is immense. Still, it is fair to say that the practical achievements of computational semantics have so far been quite limited. The reasons for that, I think, are two-fold. Automated symbolic processing of natural language is notoriously brittle: even where it is clear what the system should compute, it often lacks the necessary resources, in particular wide coverage lexicons with substantive semantic information and world knowledge in accessible form. But in many cases the problem goes deeper. We still haven’t even properly understood yet what it is that should be computed. These are hard problems, which will be solved – to the extent that they can be solved at all – only by people who have the combination of skills that are presented and taught here as parts that naturally fit into a coherent whole.

HANS KAMP
Professor of Formal Logic and Philosophy of Language, University of Stuttgart
from the furward to Computational Semantics and Functional Programming (2010) by Jan van Eijck and Christina Unger