On: Untyped Programs Don’t Exist

[AnaniasAnanas]

> most type systems don't actually reflect the subtyping relation inherent in the topos correspondent to their logic

Would you mind elaborating? With examples if possible.

> ignoring that there are piles of similar features in the language design space, like highlighting, typesetting, brace-matching, whitespace, capitalization conventions, docstrings, named variables, named procedures, 2D/spatial layout, ASCII/JIS/Unicode art, and the list goes on and on and on.

I am interested to see how any of these would protect against bugs that say a type system with dependent types would protect against.

[myWindoonn → AnaniasAnanas]

The most infamous example is that of Haskell. Reasoning in Haskell is not the same as reasoning in the category Hask [1], whose objects and arrows purport to be Haskell types and functions; many folks are actually reasoning in an idealized, simplified Hask. Papers like "Fast and Loose Reasoning is Morally Correct" [0] justify this stance. (There is, to be fair, work on determining Haskell's actual categorical properties. [2]) This attitude is popular across the ML family, but spikes in the Haskell community for some reason.

I don't have a good citation for categorical subtypes, but it is well-known category-theory folklore that often objects have subobjects and that a given arrow `f : X -> Y` has fixed source object X and target object Y, and therefore that f likely embodies not just categorical structure but also subobject structure inside X. There may be many distinct arrows of type `X -> Y`, each with different subobject behavior. This is where concepts like dependent typing shine, right?

I'm going to take the other branch of your implicit dilemma. Let's protect against the same bugs that dependent types protect against, but without dependent types. This is valid E [3] or Monte [4], and languages in the E family are what Haskellers would call "unityped" or "untyped". The specification is that `y >= x` and also that the return value `rv >= y`. The compiler is not obligated to infer corollaries like `x >= 0`.

    def f(x :Int, y :(Int >= x)) :(Int >= y) { return x + y }

It is not accidental that Monte has a categorical semantics [5] at the level of values and not types. It seems to be the case that, even if the category of types is trivial, the category of values is rich. At the same time, studying only the category of types and never examining the values is insufficient! Ponder this Haskell REPL session:

    $ nix run nixpkgs.ghc -c ghci
    GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
    Prelude> :t reverse
    reverse :: [a] -> [a]
    Prelude> :t const [] :: [a] -> [a]
    const [] :: [a] -> [a] :: [a] -> [a]
    Prelude> :t cycle
    cycle :: [a] -> [a]
    Prelude> :t map id
    map id :: [b] -> [b]
    Prelude> :t tail
    tail :: [a] -> [a]

Studying the types alone, we are helpless. We need to know something of the values as well.

[0] http://www.cse.chalmers.se/~nad/publications/danielsson-et-a...

[1] https://wiki.haskell.org/Hask

[2] http://www.cs.gunma-u.ac.jp/~hamana/Papers/cpo.pdf

[3] http://erights.org/

[4] https://monte.readthedocs.io/

[5] https://monte.readthedocs.io/en/latest/category.html