jonsterling

I agree that each ML falls short in some ways--I think SML and OCaml are probably the best programming languages ever made, but there's definitely room for improvement. I dream of the "Next Great ML"; 1ML definitely looks interesting in this regard, though I am a bit skeptical of Rossberg's rhetoric on a number of issues.

I use SML over OCaml mostly for cultural & political reasons; SML has a few areas ripe for improvement (some of which are addressed in OCaml, others not):

1. structure sharing in the Definition is so bad that pretty much all the implementations of "S"ML diverge from it in some way. Each implementation of structure sharing is frustrating in its own way.

2. would be nice to be able to do higher-kinded polymorphism, as in 1ML

3. would be nice to unify polymorphism as a mere mode-of-use of functors, as in 1ML (well, this was not invented in 1ML, as I first saw it in Dreyer/Harper/Chakravarty's "Modular Type Classes": http://www.mpi-sws.org/~dreyer/papers/mtc/main-long.pdf; it may go back as far as the Harper-Stone type theoretic semantics). Combined with higher-order functors (which I believe are proposed to be added to "Successor ML"), this would give a proper treatment to polymorphism at higher kinds.

4. we need to standardize on a package calculus; the ML Basis system as used in Mlton is pretty nice, as is the simpler system used in SML/NJ's "Compilation Manager".

5. modular type classes (analogous to coq's "canonical structures") should be added in order to alleviate the pain of explicitly instantiating functors, etc. We do NOT want "type class coherence" as in Haskell, which amounts to a piece of global state that essentially outlaws local reasoning. I call it the "Antimodularity Restriction", but the name hasn't caught on, as much as Haskell folks like to berate us over our "value restriction" (which is a non-problem, and very useful--though it would be better to reconstruct it in a less ad-hoc way, via the theory of polarization that comes from Girard, and was further developed in light of effects, refinements and polymorphism by Zeilberger in his dissertation).

6. I'd like to (at least) follow OCaml and add the ability to convert between module signatures & existential types; I'm not sure if I am sold on the 1ML approach, which goes quite a bit further than this, but I need to investigate it more.

7. Refinement types would be nice (but PLEASE---do not fix in advance some awful solver or something for this; contra the popular literature at the moment refinement types have NOTHING at all to do with solvers!).

I agree. OCaml is really cool in many respects, and I like it a lot—but the only thing SML really needs is a modern Basis library that is applicable to today's standard use-cases.

I use SML for the JonPRL proof assistant, and I couldn't be happier. Some things would be a bit easier in OCaml, but to be honest, I love the fact that my code will continue to work without modification for decades, due to the simple fact that SML is a language frozen in time.

elephants scale after all

I rely heavily on tig. highly recommended

If I share with somebody that I have an issue about something, I want to be sure that people will not conflate my legitimate complaint with my "mood".

It's a really nice way to gas-light folks into submission: "The team has noticed that your mood has been pretty poor the last few weeks; is there anything we can do to lift your spirits? We're worried that your mood is affecting your work." <---- utterly horrifying

Now, I can't say what's going on in your team, and probably at the moment, all is well and nobody is feeling victimized by this. But consider the fact that by binding up two (properly) separate concepts (reporting of blockers, etc. vs. poor emotional state, which is a PRIVATE matter), you will be ruling out a lot of potential employees in the future. Your team could decide to change the policy as they please, but if I came in for an interview and heard about this, I'd run as far as I could.

EDIT: I have worked with people who suffer from depression and mental illness. I cannot imagine how stressful a work environment like this would be for some of these folks. I've been working at startups for years, and I have a thick skin—I can "deal with" the high pressure and culturally necessitated amalgamation of one's personal and professional life (even if I hate it), but there are a lot of really skilled workers for whom this is incredibly destructive.

This sounds downright dehumanizing. fuck

I am very (twice) familiar with getting screwed because founders don't want employees to bolt while there is still a chance of recovery. The good thing was that they had the good sense to let me go before all the money totally ran out, so I was able to bridge my way to the next job, which I really appreciated.

If your company's in that position, the only ethical thing is for all employees to be well-informed of that, in advance.

I don't think this is even legal; I'm sorry for your situation, but you must see that if this sort of thing were allowed, it would pave the way for slavery.

Very little of research in programming languages is anything like “We tried it out on a bunch of developers and the data support our conclusion that ...”.

PL is not an empirical science in that sense, it's more like mathematics. So your initial intuition about type safety, etc. is right on the money—that's the academic side of it.

I assume by "academic" the other poster meant "informed by academic research". Swift is evidently more so than Objective-C.

I worry about my company going out of business more than I worry about getting fired...

In bob's setting, the computation system is not determined or fixed. It is open-ended...

In intuitionistic mathematics, we of course accept that there is no Turing computable halting oracle, but we do not rule out the possibility that there is some other effective oracle that can decide halting. (This is in contrast to recursive mathematics / Russian constructivism)

Bob is coming from the perspective of Brouwerian Intuitionism, and so he is not really that interested in a closed "formal system". So, "proofs" in the setting that Bob cares about are not derivations in a formal system, so Gödel's result doesn't really apply.

You do not in general decide whether two types are equivalent. You prove it...

Bizarre that this fellow grimaces at "type erasure". That's the correct way to polymorphism!

Do you really not see the power dynamic at play here?

can't tell if this is brilliant sarcasm

Wow, a weekend hackathon where employees worked all night (https://www.airbnb.com/careers/departments/engineering). Capital is getting smarter every year! Now you can make workers think that they were the ones who decided to do unpaid overtime.

(And if it wasn't "required", don't kid yourself---of course it was required.)

Location: Portland, OR

Remote: Yes (nine months successful remote experience)

Willing to relocate: no

Technologies: Haskell, Standard ML, OCaml, Objective-C

Résumé: http://www.jonmsterling.com/pdfs/sterling-cv.pdf

Email: jon [ at ] jonmsterling [ dot ] com

Sorry, my comment was poorly worded—I mean that I am experiencing schadenfreude, not criticizing people who are also experiencing it.

Cheers!

Oh my goodness, people are misinterpreting my comment, I am so sorry.

I mean that I am experiencing so much schadenfreude. I am not criticizing anyone else who is sharing in it.

GOD, so much schadenfreude here...

Glad somebody said it...

That it's a huge mistake to use a BaaS for anything but a demo. I think it's good to abstract out certain details that don't pertain to your application logic, and that's precisely what something like Heroku does. In my experience, a BaaS adds barely anything to that, and subtracts way more in terms of flexibility and lock-in.

The amount of administration that using a BaaS saves (as opposed to something like Heroku) is minimal; the time that you'd spend doing straightforward admin stuff is just moved over to working around limitations of the BaaS, and is often multiplied in the process. The amount of actual code that using a BaaS saves is between 100-400 lines for a web application. Awful deal.

Cool that they used FP to develop this, but haven't we already learned the lesson about the BaaS stuff?

Called it.

I make a huge difference wherever I have worked; you may ask any of my employers. However, my interest and my soul are my own; they do not belong to my employer. I do not even rent them to my employer.

But honestly, I couldn't imagine having so few interesting thoughts of my own that I would actually willingly let myself be filled up with enthusiasm for some ephemeral product, or some ephemeral business, or even worse a "vision" or a "mission". I've got better things to think about at night.

Also, re "just a worker", I am happier to be called a "worker" than any other of the made-up terms which Capital has come up with in order to divide the working class. It at least puts me in the right bucket as far as the class struggle is concerned.

BTW, don't be too broken up about me not being a suitable hiring prospect for you. I'm going to leave the hell-hole that is tech as soon as the school debts are paid, and then go do something worthwhile.

@luckydude

If anyone ever says, “I like what you are doing, I want to help”, they are probably just blowing smoke up your ass. We're workers. We want to get paid in return for labor. It's not like choosing which non-profit you want to sit on the board of.

yep.

ML.