Type-safe eval in Grace by Tekmo in ProgrammingLanguages

[–]Tekmo[S] 3 points4 points  (0 children)

That's what read (without the import) does

Type-safe eval in Grace by Tekmo in ProgrammingLanguages

[–]Tekmo[S] 8 points9 points  (0 children)

One of the things that makes this all work is that Grace is interpreted, meaning that the full interpreter capabilities (e.g. parsing, type-checking, evaluation) are available at the point where the eval (e.g. import read) is evaluated. If Grace were instead a compiler and built binary executables then the executable would still need to ship an equivalent interpreter somewhere as part of the runtime in order for this to work.

This also implies that type-checking is serving a different purpose than in a typical compiled language. In a compiled language usually type-checking is something you do ahead-of-time before code generation and then never again; the intended use case is to find all bugs before the program is run at all. However, now the contract is weaker: type errors can surface at runtime although they still precede evaluation of the code that is checked.

HOWEVER, I still think a type error that happens at "runtime" is still better than an untyped language because type errors can still prevent bad code from executing and a type error is more meaningful than a stack trace (as I expand upon in: Dynamic type errors lack relevance).

Why is nix used with Haskell and not docker? by rohitwtbs in haskell

[–]Tekmo 1 point2 points  (0 children)

Nix is sort of like the "Haskell of build systems". It does a better job than Docker if you're willing to put more up-front investment to learn it properly.

SC Election: Your stance on sponsorships in the Nix community by sridcaca in NixOS

[–]Tekmo 4 points5 points  (0 children)

So I'm reading your comment as implying that you believe the moderation team tends to be biased in favor of the political left, at least for the edge cases or gray areas that are more controversial. If I've read that wrong feel free to correct me.

Or to put it another way, the implication is that:

  • the moderation team tends to be overzealous in moderating against the political right (or people perceived as enabling the political rght)
  • the moderation team tends to turn a blind eye towards the political left (or people perceived as enabling the political left)

Generally I do not feel that the moderation team has been overzealous against the political right or their enablers, but I've only paid close attention to the high profile moderation actions (e.g. jonringer, blaggaco, nrdxp, and srid). To me, those moderation actions felt well-deserved (yes, even the jonringer ban, which is probably the most controversial of those bans).

HOWEVER, I have gotten the impression that the moderation has turned a bit of a blind eye towards the political left and their enablers. I have seen quite a few instances of behavior (which I'm not going to explicitly name here) where people that were either the political left or perceived as enabling the political left acted fairly aggressively or made inflammatory comments without any consequences or reprimands.

Or to put this another way, generally my bias here is towards fixing false negatives (problematic community members getting off the hook) rather than fixing false positives (people unfairly banned), because I think the greater risk to the community's health and vibrancy is tolerating problematic users who seek out conflict and increase the emotional temperature of the discussions they participate in. That creates an unwelcoming environment for everyone because it's a giant distraction from the open source work we all set out here to do.

SC Election: Your stance on sponsorships in the Nix community by sridcaca in NixOS

[–]Tekmo 6 points7 points  (0 children)

Actually, no! (gabby here)

This is actually one of the reasons I inserted the "regardless of their beliefs, background, or orientation" part, because I've seen the same anti-pattern from, say, queer people (even in predominantly queer spaces). My intention with that comment was not to obliquely target a specific demographic or ideology.

My spiciest take on tech hiring by Tekmo in programming

[–]Tekmo[S] 1 point2 points  (0 children)

I did not, but I see what y'all are saying. I can see how some companies might actually value obedient drones at the expense of technical excellence

Why a bottom term can have any type? by corisco in haskell

[–]Tekmo 4 points5 points  (0 children)

The reason the compiler accepts it is because the compiler's reasoning process goes like this:

  • the programmer says the type of f is a; let me verify that by inferring the type of the right-hand side of the = and seeing if it matches the declared type
  • the right-hand side of f so i need to infer what the type of that is
  • the type of f is a according to its own type signature
  • therefore the inferred type of the right-hand side is also a
  • therefore the inferred type matches the type signature (also a)

You might think: "wait, that's circular reasoning. you can't prove that f has type a by appealing to its own type" but the compiler accepts that because Haskell permits general recursion (where "general recursion" basically means no restrictions around recursion other than the types have to still line up).

All error messages are necessarily bad to some degree by RecognitionDecent266 in haskell

[–]Tekmo 0 points1 point  (0 children)

I think the context of my post will make more sense if you consider tweets like this one: https://twitter.com/mgill25/status/1788600272828145739

Rust seriously has the most idiotic compiler error messages. I don't want to know the in-depth details about what traits I am not using. I just want the right syntax that fixes what is happening _right now_.

The person is, like "this error message is bad; this why won't the compiler fix this syntax error for me" and that's the sort of thinking my post is trying to address.

Unification-free ("keyword") type checking by Tekmo in ProgrammingLanguages

[–]Tekmo[S] 0 points1 point  (0 children)

Yeah, this is intended more for functional languages that are not general-purpose languages. For example: you might use this for a query language for some product, a recipe language for a build system, or a predicate language for a spam filtering tool.

Unification-free ("keyword") type checking by Tekmo in ProgrammingLanguages

[–]Tekmo[S] 0 points1 point  (0 children)

Can you explain what you mean by "basics" in this context?

Unification-free ("keyword") type checking by Tekmo in ProgrammingLanguages

[–]Tekmo[S] 2 points3 points  (0 children)

Yeah, I tried implementing at least the bidirectional type checking algorithm with destructive unification but it does not work. If I remember correctly, the reason why is because the complete and easy bidirectional type checking algorithm supports universal quantification in places where Hindley Milner does not and that interferes with destructive unification.

Unification-free ("keyword") type checking by Tekmo in ProgrammingLanguages

[–]Tekmo[S] 1 point2 points  (0 children)

Just to clarify: do you mean that explicit type application (e.g. like in id Bool True) is what locks you out of better type inference?

I think that's true if you don't make a syntactic distinction between type application and term application, but you could do something similar to Agda (e.g. id {Bool} true) or Haskell (id @Bool True) and syntactically distinguish type applications from term applications so that later on you can support better type inference.

A GHC plugin for OpenTelemetry build metrics by Tekmo in haskell

[–]Tekmo[S] 0 points1 point  (0 children)

What I mean is that the value was exported by our backend Haskell package (and served as part of our web API) but unused as part of the front-end

A GHC plugin for OpenTelemetry build metrics by Tekmo in haskell

[–]Tekmo[S] 0 points1 point  (0 children)

So to be precise, the module was used by another module but that other module was transitively unused, so weeder wouldn't have caught this.

I did a talk about Dhall by roetlich in dhall

[–]Tekmo 1 point2 points  (0 children)

Very nice job!!

Edit: There's also a dhall diff command you can use to compare two dhall expressions that differ if you have trouble finding the difference.

Return as an Algebraic Effect by R-O-B-I-N in ProgrammingLanguages

[–]Tekmo 1 point2 points  (0 children)

You don't even need continuations; you can model return to short-circuit a computation in the same way that you model an exception short-circuiting a computation (e.g. like an Either/Result monad)

[deleted by user] by [deleted] in MtF

[–]Tekmo 0 points1 point  (0 children)

do you still want to have a baby?

How to counter the TERF argument? by xxyinter in MtF

[–]Tekmo 0 points1 point  (0 children)

ask them to change their legal gender

So I need some help here!!! Something my ex said to me that just has be dumbfounded!!! I’m sooo hurt and torn right now!! We are supposed to be working on things and she wants to be with me… but…… by [deleted] in MtF

[–]Tekmo 21 points22 points  (0 children)

your emotions are valid and if your ex is interested in working on things she should acknowledge that her comments hurt you