julesh

@julesh.mathstodon.xyz.ap.brid.gy

Applied Compositional Thinking

🌉 bridged from ⁂ https://mathstodon.xyz/@julesh, follow @ap.brid.gy to interact

@julesh.mathstodon.xyz.ap.brid.gy

Like many people I am very worried for the near future of my field. I'm not a problem solver and I think the problem solving half of the field is toxic and they are deserving of literally everything that has happened to them. But the dialectic between problem solving and theory building has […]

@julesh.mathstodon.xyz.ap.brid.gy

Here is an extremely neat definition of dependent lenses I've never seen before, as kleisli morphisms of the extension (ie. the equivalence of categories from containers to polynomial functors) considered as some exotic kind of generalised monad

record Cont where constructor MkCont base : Type fib : base -> Type record Ext (c : Cont) (y : Type) where constructor MkExt value : c.base continuation : c.fib value -> y unit : (x : c.base) -> Ext c (c.fib x) unit x = MkExt { value = x, continuation = id } extend : ((x : c.base) -> Ext d (c.fib x)) -> Ext c y -> Ext d y extend f x = MkExt { value = (f x.value).value, continuation = x.continuation . (f x.value).continuation } Lens : Cont -> Cont -> Type Lens c d = (x : c.base) -> Ext d (c.fib x) compose : Lens c1 c2 -> Lens c2 c3 -> Lens c1 c3 compose l m x = extend m (l x)
@julesh.mathstodon.xyz.ap.brid.gy

It occurs to me that if actually working AI was developed 70 years earlier, as many of the earliest pioneers of the field apparently expected, it would definitely have been immediately compromised by hyper-capitalism back then too

@julesh.mathstodon.xyz.ap.brid.gy

Reason number whatever that I already hate linux + kde coming from a mac: keyboard shortcuts for diacritics are just shit. After a ridiculous amount of trial and error I have managed to type ëẽéêèẹȩ, but as far as I can tell it is straight up impossible to type ė (a diacritic used in Lithuanian) […]

Older posts