[kmill]

> What makes you think being able to run such half-specified programs for part of the problem will actually help with answering this question?

Perhaps rocky1138 thinks this because they have experience answering this question by doing so?

I've found it can be hard to find the right type before I've written partial solutions to a problem. Just to be clear, I'm talking about recognizing the monads or functors or what have you. Even the general mathematician doesn't start by drawing the right diagram. (Though some do.) For me, "the right type" comes from abstracting partial solutions.

I think part of it is preference for certain thinking styles, like how some people like puzzles based on group theory and some on topology. If finding the right types ahead of time works for you, great! But don't be surprised that people manage to solve problems by other means.

(It could also be that the type systems in programming languages don't capture the intuitive types[1], and perhaps rocky1138 keeps them in his head while prototyping. Just because the types aren't written down doesn't mean they aren't there --- i.e., there is no need to obsess over making things real. But, it is nice to make them real so you don't have to keep them in your head anymore, or to communicate them to others more effectively.)

[1] I sort of mean intuitive in the sense of intuitionism.

[naasking]

> Perhaps rocky1138 thinks this because they have experience answering this question by doing so?

They have experience with their problem solving style, they don't have experience with every problem solving style, or even necessarily with my problem solving style. You can't infer much from that, and certainly not that typing is "not great when prototyping".

> Just to be clear, I'm talking about recognizing the monads or functors or what have you. Even the general mathematician doesn't start by drawing the right diagram.

Absolutely. But you define the type that seems to match part of the problem, then realize it doesn't fit another aspect, and you refactor it until it covers all of the properties you need. Sometimes this involves writing some code to ensure you've captured the right properties for the problem when there's an algorithmic part, certainly, but to think you've captured anything meaningful or coherent without type checking is bizarre.

Like you later say, "abstracting partial solutions" is probably a pretty common approach, but those partial solutions only come together in a coherent whole if they're typed. Otherwise they likely won't mesh well, and you're left with a mishmash of partial solutions, not a solution.

[kmill]

> They have experience with their problem solving style, they don't have experience with every problem solving style, or even necessarily with my problem solving style. You can't infer much from that, and certainly not that typing is "not great when prototyping".

I tend to grant the first person who states their opinion in absolutes the nicety of automatic insertion of "it is my opinion/experience that," because this is what they usually mean. Countering absolutes with absolutes is just confusing to me, so sorry for any misunderstanding.

> but to think you've captured anything meaningful or coherent without type checking is bizarre

I want to say "speak for yourself" here---this is rather dogmatic. Sometimes I use a formal type system, sometimes I don't, and yet in both cases I somehow manage to produce working programs. Sure, a computer-checkable type system is nice to have and gives me peace of mind when I use one, but I believe formal type systems are a posteriori describing particular safe ways of manipulating data out of all the possible ways of manipulating data. Is in inconceivable that a programmer can check their types manually, using an ad hoc intuitive type system?

> but those partial solutions only come together in a coherent whole if they're typed. Otherwise they likely won't mesh well, and you're left with a mishmash of partial solutions, not a solution.

Check your types: "If they are not typed, they won't come together into a coherent whole because they likely won't mesh well."

Truthfully, it sounds to me like your argument is the Fred Brooks quote about how the data structures imply the code. This is not exactly the same as having machine-checkable type systems, though such systems do force the issue.

[naasking]

> Is in inconceivable that a programmer can check their types manually, using an ad hoc intuitive type system?

Sure, if you don't mind an ad-hoc, informally specified, bug-ridden, slow implementation of half of a type checker that no one but you knows (and so is "intuitive" only to you... until you read this same code 3 months later).

[kmill]

What are you addressing? My position is that automatic type checkers are nice to have but not essential, and it is possible to prototype software without one. I am not arguing against their use, just what seemed to be your assertion that it is impossible to prototype/develop software without an automatic type checker. Anyway, I understand the pitfalls of not using one, but I also understand how type systems tend not to capture everything. There is no reason to be dogmatic about it: use whatever works as a tool for thought.

As I said before, "intuitive" is in the sense of intuitionism; not "easy to understand" or "obvious." A point of view: formal type systems comes from explaining what we see with mental perception (intuition). What do you do if your automatic type checker doesn't check every possible thing you want to verify is correct? Surely you aren't just blind to the types they "should" be. Seeing the invariants which must hold is seeing the intuitive type.

> if you don't mind an ad-hoc, informally specified, bug-ridden, slow implementation of half of a type checker that no one but you knows

I can't tell if I was understood or if you just wanted to quote Greenspun's tenth rule whether it completely worked or not: I was talking about a programmer with a type theory, not implementing an automatic type checker from scratch.

[naasking]

> My position is that automatic type checkers are nice to have but not essential, and it is possible to prototype software without one.

Sure, it's possible to prototype in the untyped lambda calculus too, or in Brainfuck. Why would you want to though?

> I am not arguing against their use, just what seemed to be your assertion that it is impossible to prototype/develop software without an automatic type checker.

I never said it was impossible, I merely implied that it was bizarre to even want to do so (among other things). Programming is hard enough as it is, why waste your time and mental energy checking properties that can be checked for you?

> I was talking about a programmer with a type theory, not implementing an automatic type checker from scratch.

A type theory in their head, in the intuitionistic sense, that they check as they're programming, not one that's actually checked by a tool is what I assumed.

And certainly you're working within limitations dictated by your language, but you can take typically it further than most think. See for instance, the paper lightweight static capabilities.