Hacker News Reader

Comment by pjdorrell | Hacker News Reader

In Python

type(type) is type

evaluates to True. And that is not permitted in mathematical type theory that the Curry-Howard correspondence applies to.

View on HN

Although it itself is deprecated, the TypeInType extension does exist.

https://www.seas.upenn.edu/~sweirich/papers/fckinds.pdf

https://www.reddit.com/r/haskell/comments/4180k3/what_is_typ...

And the only reason the language pragma is deprecated is because TypeInType is now just how things are, by default, with no opt-out.

On lobste.rs somebody pointed out that undefined satisfies the Curry Howard correspondence for Haskell, and I was wondering whether the proper analogue for Python would be NoneType in that case.

Comment here: https://lobste.rs/s/ovebeq/pythonista_s_review_haskell#c_gz0...

What Python and other dynamically typed languages call "types" aren't types at all in the theoretical sense. In type theory, types are properties ascribed to programs that describe their behavior and are part of a language's static semantics (AKA checked at compile time). Dynamically typed languages are really untyped (or from a certain perspective, "unityped," meaning that every expression has the same type: https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...).

This is a very interesting perspective! I’ve never thought about dynamic languages as a single typed static language. Thank you for sharing!

Note many dynamically typed languages have static types. Objective-C, Java, TypeScript, Dart, etc. The dynamic types bring new capabilities above and beyond what is possible with static types.

(That is, the dynamic-or-static choice is a product type, not a sum type!)

> The dynamic types bring new capabilities above and beyond what is possible with static types.

Not really. "Dynamic type" just means an object that carries around a description of its structure (or more commonly, a pointer to a description). You can do the same thing in many languages with static types. (Including Haskell. GHC has special support for this pattern.)

What special support does GHC have?

GHC can derive a Typeable type class instance for any data type which allows values of that type to be stored in a Dynamic wrapper. For soundness reasons the Typeable type class is special in that it can only be derived; you can't implement it manually. The runtime types of Dynamic values can be queried and compared and you can attempt to extract a specific known (concrete) type, which will succeed only if the runtime type matches. There are some limitations; for example, you need to know the exact type of the value you're extracting, not just a type class constraint, so you can't e.g. add two Dynamic values directly even if they hold the same type of value at runtime with a valid Num instance.

Alternatively, you can just define a recursive sum type expressing all the possible runtime types of the dynamic expression. In Aeson for example there is a type which can encode any value which might be found in a JSON file, which is basically everything you can express in Javascript apart from function closures. This doesn't require any special support from GHC and works well in most statically-typed languages.

I've heard this called "unit typed" (see the Wikipedia page of this name), I think unitype may be incorrect.

i.e. Haskell includes the unit type ()

Haskell's unit type is what other languages call "void", the type with exactly one value (not counting 'undefined', Haskell's dirty little not-secret). That's different from Unitype/Any, the type that contains all values.

Bob Harper uses "unitype" which is a pretty strong argument for the name's validity

> not counting 'undefined', Haskell's dirty little not-secret

There is no "undefined" value in pure Haskell. There are expressions that have no value, due to a runtime exception (error, undefined, division by zero, memory allocation failure) or non-termination (unbounded recursion). Either way, evaluating the expression does not produce a value for the remainder of the program to operate on—you can't write a (pure) program like `if isUndefined expr then x else y` since—assuming isUndefined is a pure function and doesn't ignore its argument—the whole program is undefined if expr is undefined.

Reply on news.ycombinator.com