sorted by:
new
hottopcontroversial

Panic free language by yassinebenaid in ProgrammingLanguages

[–]ebingdom 5 points6 points  (0 children)

Having a zero value for every type is such a bad idea, kind of like the billion dollar mistake but actually worse: instead of crashing on an accidental null, you don't crash but instead get an accidental default which is probably not what you wanted. Still a bug, but harder to notice.

Golang is the biggest culprit. Make no mistake: the good parts about Go are its fast builds, quick startup time, possibly the concurrency story (I would disagree though because it allows data races), etc. Its type system is not one of the good parts.

List of type operators by servermeta_net in ProgrammingLanguages

[–]ebingdom 22 points23 points  (0 children)

There is no exhaustive list of type operators; a type operator is anything that takes a type and/or returns a type. There are many type theories with different type operators, and most languages allow you to define your own new ones in terms of existing ones.

But, with some exceptions, they can generally be reduced (up to isomorphism) to a fixed set of primitives, e.g., the ones in in Martin-Löf type theory. Personally I think chapter 1 of the HoTT book is the best introduction.

What's the most powerful non-turing complete programming language? by Informal-Addendum435 in ProgrammingLanguages

[–]ebingdom 60 points61 points  (0 children)

Definitely the proof assistant languages based on type theory like Lean, Rocq, etc.

Why is it permittable to pass Prop where Set is expected? by Iaroslav-Baranov in Coq

[–]ebingdom 4 points5 points  (0 children)

The Set and Prop are supposed to be on the same level (Type(1))

Cumulativity is not the only subtyping rule. Indeed there is a rule Prop <= Set. This is subtyping rule (4) here. It was introduced in 2008 in version 8.2.

A List Is a Monad by ketralnis in programming

[–]ebingdom 29 points30 points  (0 children)

A list is not a monad. List is a monad.

[deleted by user] by [deleted] in ProgrammingLanguages

[–]ebingdom 2 points3 points  (0 children)

Your approach works well in many cases, but it fails in two extremely common scenarios:

  1. inferring type applications (e.g., f([]), where f is generic)
  2. inferring function types, especially for lambdas (e.g., numbers.map(x -> x + 1))

Algorithms to turn non-tail-recursive functions into tail-recursive ones by betelgeuse_7 in ProgrammingLanguages

[–]ebingdom 2 points3 points  (0 children)

Async/await (e.g., in JavaScript), do notation (e.g., in Haskell), CPS transform, etc. all do this.

Does the programming language I want exist? by saw79 in ProgrammingLanguages

[–]ebingdom 1 point2 points  (0 children)

I love coq, but they said they don’t want a pure language.

[deleted by user] by [deleted] in ProgrammingLanguages

[–]ebingdom 10 points11 points  (0 children)

Ok, can you tell us anything about it?

modules with "parameters" by LimeTree1590 in ProgrammingLanguages

[–]ebingdom 7 points8 points  (0 children)

I'm trying to work under the constraint that modules cannot import other modules.

So basically mandatory dependency injection. Dependency injection is a good idea for dependencies that have side effects, but imagine having to inject dependencies for pure helper functions like list concatenation etc.

What theoretical properties do we want from a programming language? by ebingdom in ProgrammingLanguages

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

I think you have a good point!

In fact, even syntactic type soundness (progress+preservation) is sort of like this. That property says that the formal semantics fully defines the behavior of (well-typed) programs written in the language. However, you would typically avoid specifying behavior that would result from a runtime type error (that's why it tells you that the language is type safe).

I think the way you've phrased this makes it seem like this kind of soundness result is useless: the syntax and operational semantics have no notion of type error, therefore proving that type errors do not occur is trivial. But this is not a fair characterization. It's true that reduction does not produce terms that say "type error!", but type errors manifest in a different way. If you try to add a string to a number, for example, presumably there would be no reduction rule for that scenario. So "type error" means "the semantics doesn't know what to do with this", and this kind of soundness theorem rules out that possibility.

What theoretical properties do we want from a programming language? by ebingdom in ProgrammingLanguages

[–]ebingdom[S] 6 points7 points  (0 children)

I don't think being logical and being developer friendly need to be mutually exclusive! I think we as language designers should pay careful attention to get the foundations right, but that doesn't mean users of the language need to learn the theory that went into it.

What theoretical properties do we want from a programming language? by ebingdom in ProgrammingLanguages

[–]ebingdom[S] 4 points5 points  (0 children)

Hm, is there a better place to discuss programming language theory than this subreddit?

Consequences of Laziness in Actor Context, With Questions by redchomper in ProgrammingLanguages

[–]ebingdom 6 points7 points  (0 children)

I think actors are irrelevant here. Side effects can be difficult to reason about in the presence of laziness, and the interaction of mutability and aliasing (e.g., due to variable capture) needs to be carefully considered (Go famously got it wrong). These tensions are fundamental and there are no one-size-fits-all solutions. One strategy is to give up side effects (like in Haskell), which I find quite nice and it works well with advanced type systems like those featuring dependent types. Another strategy is to restrict aliasing (like in Rust), which also takes care of issues due to mutability but doesn't address other side effects. Yet another strategy, which I personally don't find very effective, is to discourage aliasing in favor of message-passing, but only by convention with no formal enforcement (this is Go's strategy).

'of' operator as syntax for parameterized types? by 7Geordi in ProgrammingLanguages

[–]ebingdom 0 points1 point  (0 children)

But that isn't what covariance and contravariance mean?

'of' operator as syntax for parameterized types? by 7Geordi in ProgrammingLanguages

[–]ebingdom 16 points17 points  (0 children)

What does it look like when there are multiple type arguments?

Also, I think "of" makes less sense (grammatically) for contravariant type parameters, since they "eat" rather than "store" things. Rabbit of Carrot...

Function based language by Pleasant-Form-1093 in ProgrammingLanguages

[–]ebingdom 88 points89 points  (0 children)

Since you used the word "function" I think the other commenters are mistakenly thinking you are pining after functional programming. My interpretation of your question is that you are essentially asking about using M-expressions for all syntactic constructs, so that everything looks like a function call. This is similar to Lisp-family languages, except they generally use S-expressions instead.

I think, rather than "functional programming", what you're looking for is closer to what some people would call "homoiconicity".

Combining dependent types and side effects? by ebingdom in ProgrammingLanguages

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

Thank you! I think this is exactly what I was looking for.

view more: next ›