Haskell говорит правду
-- An iso for a type b is a five-tuple: (a,f,g,s,t) where -- a : U -- f : a -> b -- g : b -> a -- s : forall (y : b), f (g y) = y -- t : forall (x : a), g (f x) = x mkIso :: Val -> Val mkIso vb = eval rho $ Sigma $ Lam "a" U $ Sigma $ Lam "f" (Pi (Lam "_" a b)) $ Sigma $ Lam "g" (Pi (Lam "_" b a)) $ Sigma $ Lam "s" (Pi (Lam "_" b) $ PathP (PLam (Name "_" b) (App f (App g y))) $ Pi (Lam "x" a $ PathP (PLam (Name "_") a) (App g (App f x)) x) where [a,b,f,g,x,y] = map Var ["a","b","f","g","x","y"] rho = upd ("b",b) emptyEnv
На изображении показан фрагмент кода на Haskell, формализующий изоморфизм между типами через пятёрку значений и доказательства. Шутка в том, что для незнакомого с Haskell человека это выглядит как непонятная математическая запись, хотя подпись утверждает, что код якобы содержит оскорбление. Такой мем отправляют как nerd-шутку программистам и как реакцию на слишком сложный или непонятный код. EN: The image shows a Haskell code fragment formalizing an isomorphism between types using a five-tuple of values and proofs. The joke is that to someone unfamiliar with Haskell it looks like incomprehensible mathematical notation, while the caption claims that the code supposedly contains an insult. This meme is shared as a nerd joke among programmers or as a reaction to overly complex, unreadable code.
- @profunctor_io / 313 2017-10-01
- Type
- image
- Size
- 800×332 · 52.4 KiB
- Mood
- абсурдный, саркастичный
- Language
- en
- Added