@boarders@mathstodon.xyz
@boarders@mathstodon.xyz avatar

boarders

@boarders@mathstodon.xyz

Interested in mathematics (homotopy theory, category theory, topos theory), programming languages and philosophy

This profile is from a federated server and may be incomplete. Browse more on the original instance.

sc_griffith, to random
@sc_griffith@mathstodon.xyz avatar

no

boarders,
@boarders@mathstodon.xyz avatar

@sc_griffith this is why I love mathematics

oantolin, to random
@oantolin@mathstodon.xyz avatar

I can't believe I never noticed before that the fundamental group of a join of non-empty spaces is always free. If X and Y have m and n components respectively, then the fundamental group of XY is free on (m-1)(n-1) generators. I think I only knew the case where m or n is 1, where XY is simply connected.

boarders,
@boarders@mathstodon.xyz avatar

@oantolin this is a nice fact (and one I also didn’t know), but I haven’t quite yet convinced myself why it is true (I think one can probably directly give the cells of a CW complex of the join, but somehow I don’t think this is a nice way to think of it)

boarders,
@boarders@mathstodon.xyz avatar

@oantolin a very slick argument :)

deech, to random
@deech@mastodon.social avatar

Esolang where literally everything is called functor

boarders,
@boarders@mathstodon.xyz avatar

@deech the functor module signature is a functor for endomap on which we might make it into a functor by writing fmap by overloading the operator()

alexr, to random

So how free could a monad be, in principle? Could you make them even freer, if you wanted? Or are these as free as we're getting?

boarders,
@boarders@mathstodon.xyz avatar

@chrisamaphone @alexr “obedience to a law one has prescribed for oneself is freedom” - Rousseau thinks the answer is algebras

boarders, to random
@boarders@mathstodon.xyz avatar

“Philosophers today are as fond as ever of apriori arguments with ethical conclusions. One reason such arguments are always unsatisfying is that they always prove too much; when a philosopher 'solves’ an ethical problem for one, one feels as if one had asked for a subway token and been given a passenger ticket valid for the first interplanetary passenger-carrying space ship instead.”

chrisamaphone, to random
@chrisamaphone@hci.social avatar

me clicking “show more” on a post from a server with no length limit: i have been tricked into reading a blog post. how dare

boarders,
@boarders@mathstodon.xyz avatar

@beka_valentine @chrisamaphone incredibly punishing memories from 2013 of reading that utter drivel

typeswitch, to random
@typeswitch@gamedev.lgbt avatar

thinking about separating representation types from reasoning types

boarders,
@boarders@mathstodon.xyz avatar

@typeswitch @MartinEscardo lean4 has some of this idea (i.e. using C arrays to represent lists in compiled programs). The thing I would like with this is some kind of process of formal refinement where I can construct a program by some specification of pattern matching and I can allow certain type refinements of an interface that meet this specification. I think this is a kind of (somewhat unfulfilled )vision of algebraic programming offered by ML-style modules.

boarders, to random
@boarders@mathstodon.xyz avatar

A strange dogma that entered parts of culture through analytic philosophy is the notion that some special status is afforded a view which is presented in the form of a collection of premises and conclusion (all in quasi-legalistic ordinary language) in some ambient logic which is not to be further commented upon.

This is transformed from the reasonable seeming view that clarifying constituent parts of an argument can help us to understand the stakes of a debate/position and to clarify which aspects of a worldview are in play, into the view that doing this performance demonstrates some higher adherence to truth or some higher standards of rigour. I see no reason why stories, myths, parables, dialogues, aphorisms, argumentative essays etc. cannot be as good or better at investigating some question than pretend logical syllogisms.

boarders,
@boarders@mathstodon.xyz avatar

“The extreme deductivism of much contemporary analytic philosophy may reflect the grip of the problem/solution metaphor”

chrisamaphone, to random
@chrisamaphone@hci.social avatar

do you have an onion opinion

boarders,
@boarders@mathstodon.xyz avatar

@chrisamaphone hard to articulate as it is very multi-layered

jntrnr, to random

Something I'm noticing in comments to my recent blog post on is that a lot of folks have a strict separation between interactive shell and scripting.

When I point out in the post that Nushell is really meant to scale smoothly between the two, some folks say things like "so you're saying it's really a scripting language not a shell"

I want to help folks see they don't have to choose. They can scale ideas all the way up in one language without rewriting.

boarders,
@boarders@mathstodon.xyz avatar

@jntrnr if it is a scripting language, then I would say it resolves the fundamental tension of scripting langauages, which is to treat pipes and processes as a kind of ffi interface which we can marshall data and invocations back and forth to but which are fundamentally separate. Scripting langauages (other than something like #lang rash, in racket) don’t seem to have resolved this distance between other process calls, environment variables etc. and those things which lie firmly within the programming language.

I think one reason people are resistant to these kinds of programming environments is that current thinking on language design has led to a kind of dogma of responsibilities- you should read data from the “outside world” - keep it inside the sealed off world of the programming language for as long as possible, and then convert back to something the outside world speaks. It is not as though this isn’t in some sense a good model or “true”, but there is no reason not to question it as a fundamental design principle (as excel, smalltalk, common lisp and nushell all, to some extent, do in my mind)

wilfredh, to random
@wilfredh@mastodon.social avatar

Rust is the only language I can think of with a first party version switcher. rustup is maintained by the core team, unlike rvm or nvm.

Are there other languages like Rust in this respect?

boarders,
@boarders@mathstodon.xyz avatar

@wilfredh perhaps ocaml with opam

todd, to random
@todd@mathstodon.xyz avatar

Hello everyone! I have arrived on Mathstodon now.

If you're in the fortunate position of not knowing me, I am a Teaching Fellow and (until my corrections are done) Ph.D. student at the University of Birmingham, in the School of Computer Science's Theory Group. I am interested in constructive mathematics, univalent type theory and Agda.

My first bit of news is that yesterday I successfully defend my thesis (subject to minor corrections), which concerns formally reasoning in Agda about search algorithms on types for exact real numbers. I was supervised by Dan Ghica and @MartinEscardo.

boarders,
@boarders@mathstodon.xyz avatar

@todd really looking forward to reading it after your excellent related blog posts! Congrats and good luck for what lies next!

jonmsterling, to random
@jonmsterling@mathstodon.xyz avatar

Today is my first day of work as Faculty! Wish me luck

boarders,
@boarders@mathstodon.xyz avatar

@jonmsterling good luck Jon! Make your own history :)

zanzi, to random

I was pretty excited that HoTT has finally started to click for me, but the neverending joyless comments that I need to rename my monoids to pointed magmas is killing any interest in the topic

boarders,
@boarders@mathstodon.xyz avatar

@zanzi I understand the frustration. What helps me is to understand that social media as a technology creates some sense of immediacy without any of the usual context that accompanied immediacy. People will assume an idle observation or scratchpad thought is some kind of official record of note or tally of your knowledge.

boarders, to random
@boarders@mathstodon.xyz avatar

In the same way as we should (or have) do(ne) away with the dualisms of analytic vs synthetic, fact vs value and empirical vs theoretic (and doing away with a dualism doesn’t mean doing away with all relevant distinctions), I think it is worth questioning the dualism of formal vs informal. We reason about “formal” systems by meta-theoretic principles which are arrived at via informal reasoning or informal arguments. It is not clear what the meaning of “can be formally proved in principle” is in almost all cases, and it is not clear that it is valuable in itself. There remains value in the idea of more reliable or truthworthy knowledge and in the immense capacity formal systems seem to grant us.

sanityinc, to haskell
@sanityinc@hachyderm.io avatar

This article very much echoes my own position on #Haskell these days. From what I can tell after a number of years in the space, the practical Haskell-in-industry folks are gradually dispersing to other language communities. https://journal.infinitenegativeutility.com/leaving-haskell-behind

boarders,
@boarders@mathstodon.xyz avatar

@ocramz @sanityinc I think it also is just a natural phenomenon of people of a certain age with changing priorities or a desire to explore elsewhere. That is fine, but frustrating that it is treated as some telling trend. I also feel that Rust does a huge amount of heavy lifting in these discussions since it is understated that almost no langauages have good ecosystems, good tooling etc.

BartoszMilewski, to random
@BartoszMilewski@mathstodon.xyz avatar

So now I'm convinced that not every endofunctor in a CCC is self-enriched and, consequently, strong. So why are Haskell functors strong? What's the secret spice?

boarders,
@boarders@mathstodon.xyz avatar

@BartoszMilewski @antidote @MartinEscardo it is also the case that fmap in Haskell will satisfy “free theorems”. In particular, any potential Haskell function with the fmap signature satisfies the functor laws iff it satisfies the identity law (fmap id === id). This law is not true in a general category (just come up with any old bad choice, say using excluded middle, of function Ar(C) -> Ar(D) which preserves identity)

chris__martin, to random
@chris__martin@functional.cafe avatar

Have a theory that one of the chief benefits of remote work - possibly not a benefit for all types of work - is that people haven't been amped up by drivers' aggression

boarders,
@boarders@mathstodon.xyz avatar

@chris__martin I do think there is something - I don’t know what - with driving a car that brings about a pathological disposition in people (and probably worse in those drawn more easily to anger). Otherwise mostly normal people will suddenly start screaming or becoming needlessly violent in intent towards those around them even for what the driver knows to be a mistake or incompetence

boarders, to random
@boarders@mathstodon.xyz avatar

Are there any CS courses or books which concentrate on “design” - not necessarily in the sense of software engineering and thinking about good design of a codebase (though that is not irrelevant), but meaning “design” in terms of “user”-design e.g. library design, DSL design or application design (e.g. I could imagine such a course based around re-thinking some part of computing like text editing, version control, unix utilities etc. from the ground up and thinking about what is a good approach to their design)?

One recent book in this vein is Software Design For Flexibility by Hanson and Sussman. Another line of thinking I am a fan of is Conal Elliott’s ideas about denotational design. I think some of the ideas from Goguen are also relevant to an “algebra of design”. I would love to know some other references or points of view.

boarders,
@boarders@mathstodon.xyz avatar

@abcdw thank you for the suggestion! I’ll have a look

suppi, to random

An important aspect of 'project maintenance' is figuring out what the code is doing after being away for a while (debugging).

In the Haskell world since we don't have a step-deubgger our tools for figuring out what's going on are reading code and simulating it in our heads, and trace debugging (printing values at useful locations).

I often have a hard time simulating complex flows in my head, so I use trace debugging a lot to have a concrete scenario from which I can extrapolate.

boarders,
@boarders@mathstodon.xyz avatar

@suppi I really wish we had runtime support for debug logging or well-supported debug macros in Haskell. Laziness makes it challenging, but we shouldn’t be at a disadvantage to C in understanding our programs

boarders, to random
@boarders@mathstodon.xyz avatar
BartoszMilewski, to random
@BartoszMilewski@mathstodon.xyz avatar

If every coin toss produces both heads and tails (as in zero gravity), there's no sense in assigning probabilities. If I'm ending up in both universes, after a quantum experiment; probability loses its meaning. Probability only makes sense if one outcome excludes the other.

boarders,
@boarders@mathstodon.xyz avatar

@BartoszMilewski I think it does make sense, but it means that probability becomes purely about the epistemic. For example, if I toss a coin and then don’t show you the outcome, what probability should you assign to it? That said, I think purely subjective accounts of probability (Bayesianism) don’t seem quite right, since it is unclear why we should assign uniform probabilities to symmetric situations.

  • All
  • Subscribed
  • Moderated
  • Favorites
  • •
  • JUstTest
  • everett
  • magazineikmin
  • mdbf
  • thenastyranch
  • khanakhh
  • rosin
  • Youngstown
  • ethstaker
  • slotface
  • modclub
  • kavyap
  • DreamBathrooms
  • Durango
  • provamag3
  • ngwrru68w68
  • InstantRegret
  • tacticalgear
  • GTA5RPClips
  • cubers
  • normalnudes
  • osvaldo12
  • tester
  • anitta
  • cisconetworking
  • megavids
  • Leos
  • lostlight
  • All magazines
    •