Tests aren’t enough: Case study after adding type hints to urllib3 • Hacker News Board

Re: Tests aren’t enough: Case study after adding type hints to urllib3

#201

Post by native_samples » Wed, Oct 20, 2021, 10:10 AM UTC

tehnub wrote: post #195

native_samples wrote: post #185

Earlier quoted context omitted.

No, but that isn't required for a static type system. Most languages would just unify to the top type.

Could you elaborate on that? It sounds like I may have an overly simplified understanding of the topic here—wouldn't be the first time.

Static type systems don't imply fully dependent types. In Kotlin:

    sealed class Program
    class HaltingProgram : Program()
    class InfiniteProgram : Program()

    fun checkIsHalting(p: ByteArray) = if (halts(p)) HaltingProgram() else InfiniteProgram()

This program will type check just fine. The inferred return type will be Program because that's the nearest shared ancestor type of both possible return types. Good luck implementing the halts() function of course, but that's not the type system's problem.

Re: Tests aren’t enough: Case study after adding type hints to urllib3

#202

Post by freemint » Wed, Oct 20, 2021, 10:53 AM UTC

kennywinker wrote: post #149

freemint wrote: post #49

Earlier quoted context omitted.

Sounds like a brilliant case for multiple-dispatch.

Right so we have: function find_user(person: string) and also: function find_user(person: Object) how long before someone writes this: find_user(person: { name: "dave" }) meanwhile, someone else, not suspecting that they'll be handed a weird half-formed `User` object adds `person.id` somewhere in the body of the Object version of `find_user` and now we have a weird edge-case where very rarely `find_user` panics becau…

Multiple dispatch and compile time times are not exclusive at all.

Re: Tests aren’t enough: Case study after adding type hints to urllib3

#203

Post by tetha » Wed, Oct 20, 2021, 7:47 PM UTC

native_samples wrote: post #185

tehnub wrote: post #184

Earlier quoted context omitted.

It's the return type that isn't decidable. You can't statically check, in the arbitrary case, whether the function returns an int or a string.

No, but that isn't required for a static type system. Most languages would just unify to the top type.

Yes, but it is not required that a type system has a singular top type. It is entirely valid for a type system to have any number of types which are not in any sub- or supertype relationship.

And once there are two types T1 and T2 which are neither subtypes, nor supertypes of each other, and 2 expressions A1 and A2 of types T1 and T2, and a statically undecideable expression p, then statically typing "if p then A else B" is a problem.

And yes, I agree: Most if not all practical type systems will not accept an if-else statement if they cannot unify both branches of the conditional into a single type. Which makes sense. Because you have to act on the result of the expression, and then it needs to have some common type.

But on a purely theoretical basis, it is entirely possible and valid to have an undecideable type system. Which, btw, happens for a lot of languages: https://3fx.ch/typing-is-hard.html . There are C++ programs which are provably impossible to type at compile time.

Re: Tests aren’t enough: Case study after adding type hints to urllib3

#204

Post by kennywinker » Thu, Oct 21, 2021, 7:32 PM UTC

freemint wrote: post #202

kennywinker wrote: post #149

Earlier quoted context omitted.

Right so we have: function find_user(person: string) and also: function find_user(person: Object) how long before someone writes this: find_user(person: { name: "dave" }) meanwhile, someone else, not suspecting that they'll be handed a weird half-formed `User` object adds `person.id` somewhere in the body of the Object version of `find_user` and now we have a weird edge-case where very rarely `find_user` panics becau…

Multiple dispatch and compile time times are not exclusive at all.

I'm saying the problem isn't solved by multiple dispatch alone, but it is solved by compile time types alone. You can use both together, of course.

Re: Tests aren’t enough: Case study after adding type hints to urllib3

#205

Post by freemint » Fri, Oct 22, 2021, 10:41 PM UTC

kennywinker wrote: post #204

freemint wrote: post #202

Earlier quoted context omitted.

Multiple dispatch and compile time times are not exclusive at all.

I'm saying the problem isn't solved by multiple dispatch alone, but it is solved by compile time types alone. You can use both together, of course.

The issue whether the language is interpreted or compildd (which would distinguish compile time types from strong types) is in my opinion completely orthogonal to the issue of how dispatch works. Strong types and multiple dispatch fix the issues I see even in an interpreted language.