4 ms·

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.

yingw787 7y ago
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_gz09vc https://lobste.rs/s/ovebeq/pythonista_s_review_haskell#c_gz0...
- TheAsprngHacker 7y ago
  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-languages-are-static-languages/ https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...).
  - yingw787 7y ago
    This is a very interesting perspective! I’ve never thought about dynamic languages as a single typed static language. Thank you for sharing!
  - ridiculous_fish 7y ago
    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!)
    - greydius 7y ago
      > 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.)
      - giornogiovanna 7y ago
        What special support does GHC have?
        nybble41 7y ago
        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.
  - correct_horse 7y ago
    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 ()
    - lonelappde 7y ago
      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
      - nybble41 7y ago
        > 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.
pdexter 7y ago
Although it itself is deprecated, the TypeInType extension does exist. https://www.seas.upenn.edu/~sweirich/papers/fckinds.pdf https://www.seas.upenn.edu/~sweirich/papers/fckinds.pdf https://www.reddit.com/r/haskell/comments/4180k3/what_is_typeintype/ https://www.reddit.com/r/haskell/comments/4180k3/what_is_typ... https://www.reddit.com/r/haskell/comments/4180k3/what_is_typeintype/cz0onpy/ https://www.reddit.com/r/haskell/comments/4180k3/what_is_typ...
- matt-noonan 7y ago
  And the only reason the language pragma is deprecated is because TypeInType is now just how things are, by default, with no opt-out.

yingw787 7y ago

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_gz09vc https://lobste.rs/s/ovebeq/pythonista_s_review_haskell#c_gz0...

TheAsprngHacker 7y ago
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-languages-are-static-languages/ https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...).
- yingw787 7y ago
  This is a very interesting perspective! I’ve never thought about dynamic languages as a single typed static language. Thank you for sharing!
- ridiculous_fish 7y ago
  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!)
  - greydius 7y ago
    > 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.)
    - giornogiovanna 7y ago
      What special support does GHC have?
      - nybble41 7y ago
        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.
- correct_horse 7y ago
  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 ()
  - lonelappde 7y ago
    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
    - nybble41 7y ago
      > 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.

pdexter 7y ago

Although it itself is deprecated, the TypeInType extension does exist. https://www.seas.upenn.edu/~sweirich/papers/fckinds.pdf https://www.seas.upenn.edu/~sweirich/papers/fckinds.pdf https://www.reddit.com/r/haskell/comments/4180k3/what_is_typeintype/ https://www.reddit.com/r/haskell/comments/4180k3/what_is_typ... https://www.reddit.com/r/haskell/comments/4180k3/what_is_typeintype/cz0onpy/ https://www.reddit.com/r/haskell/comments/4180k3/what_is_typ...

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