I finally get types

A place to discuss the science of computers and programs, from algorithms to computability.

Formal proofs preferred.

Moderators: phlip, Moderators General, Prelates

4=5
Posts: 2073
Joined: Sat Apr 28, 2007 3:02 am UTC

I finally get types

"Type" is just another name for anything you've proven about the value at that point in the program.
If I needed to display comments on my blog I could use types make sure that I never display comments that do dangerous things.

Code: Select all

`newtype UnsafeString = UnsafeString Stringnewtype SafeString = SafeString Stringrequest :: String -> IO UnsafeStringhtmlEncode :: UnsafeString -> SafeStringwrite :: SafeString -> IO ()`

similarly

Code: Select all

`if(x < 5)    At this point you have proved x is less than five.else    At this point you have proved x is five or more.So you can have different operations that depend on whether x's type is "less-than-five" or "not-less-than-five".`

Really any arbitrary thing about a value can be one of its types as long as its something that you can prove.

Sorry if this isn't useful, but I'm just so happy now that I can finally see how parametric polymorphism, structural types, uniqueness types and the difference between a string and integer are all one simple concept.
Please tell me if there are interesting things called types that are not about what you can prove.

Posts: 3072
Joined: Mon Oct 22, 2007 5:28 pm UTC
Location: Beaming you up

Re: I finally get types

You've just encountered the Curry-Howard Isomorphism. When programming, all a type will typically mean "this is what kind of thing this thing is". Any type system can be trivially converted to an equivalent system of logic, so it stands to reason that once you get a sufficiently interesting type system, you also get a sufficiently interesting logical system. To do logic programming, we encode a proposition in the type of our program, and if we can write a value of that type which the compiler accepts, we have proven that proposition.
We can actually pick apart Haskell's type system and find some problems that make it problematic as a system of logic. We'll start with the basics:

Code: Select all

`-- (a, b) == (A and B), which can also be written (A × B)data (,) a b = (a, b) -- we can make a true (a, b) by providing proofs (values) of type a, b-- Either a b == (A or B), which can also be written (A + B)data Either a b = Left a | Right b -- we can make a true (Either a b) by providing a proof of type a, OR a proof of type b-- (a -> b) == (A implies B), which can also be written as (A → B)-- given a proof (value) of type a, we get a proof (value) of type b`

To finish our correspondence with propositions, we need universal quantification. From the type perspective, "∀" is a way of bringing type variables into scope. Haskell has type variables, but hides the quantification for us. We will turn off that hiding later on, and see that GHC uses the "forall" keyword for this purpose.

Implication is where things start to go wrong for us, in Haskell. Let's take a look at some obvious implications. You'll want to be using a specific invocation of ghci for this:

Code: Select all

`\$ ghci -fprint-explicit-forallsλ> :t id -- ∀a. a → aid :: forall a. a -> aλ> :t const False -- ∀b. b → Boolconst False :: forall b. b -> Boolλ> import Data.Functionλ> :t fix -- this one is interesting... ∀a. (a → a) → afix :: forall a. (a -> a) -> a`

The type of fix is somewhat worrying. We (or rather, the standard library) have proved that if a thing implies itself, that thing is true. Do we have any of those implications lying around? Why yes!

Code: Select all

`λ> :t fix id -- oh god, whatfix id :: forall a. a`

Everything is true! This is usually okay, because even if our logical system is unsound, it stops a lot of "obviously false" proofs. For most programming, the type system only needs to make the distinction between "no obvious bugs" and "obviously no bugs".

For an example of a logically sound language, see Agda, but there's a catch. By rejecting all false proofs, Agda loses the ability to prove some true propositions. Oddly, this also means Agda isn't Turing-complete. As it happens, Gödel's incompleteness theorem in logic corresponds to the halting problem in general programming.

Agda includes many interesting features that help the programmer work around those limitations and convince it of a proof's soundness. Just be prepared for a fairly rough time learning, as it's not yet made it from "learning through research papers" to "learning with tutorials".
<quintopia> You're not crazy. you're the goddamn headprogrammingspock!