P could even be a false statement, Q would still be true if P were true, so the implication P → Q is not considered to be proved wrong. If Q is some statement that is always true, no matter what the circumstances - like 'the sun is hot' - then it doesn't matter what P is. We'll often use letters to stand for entire statements, so for example if W is the statement 'the weather is nice', and T is the statement 'we'll walk into town', then we could say W → T. For example, our earlier statement could be recast as ' x is positive → x has a real square-root ', meaning the number's positivity implies the existence of the desired kind of root. We use the A→B sign (read as 'A implies B') to indicate that B is true whenever A is true. Formal logic is a way of representing statements which approximate English meanings with a Boolean logic on which we can do computations. These kinds of statements also crop up in mathematics we can say things like 'If x is positive, then it has a (real) square-root'. For example, 'If the weather is nice today, then we'll walk into town'. In everyday language we use a lot of 'If. This is a very brief introduction for a wider grounding we recommend you consult an introductory textbook on the subject matter. We need some background on formal logic before we can begin to explore its relationship to type theory. But what is the nature of this correspondence? What does a type like a -> b mean in the context of logic?Ī crash course in formal logic Incredibly, it turns out that a type is only inhabited when it corresponds to a true theorem in mathematical logic. For example, there is no function with type a -> b, because we have no way of turning something of type a into something of a completely different type b (unless we know in advance which types a and b are, in which case we're talking about a monomorphic function, such as ord :: Char -> Int).
We might want to ask the question: given an arbitrary type, under what conditions does there exist a value with that type (we say the type is inhabited)? A first guess might be 'all the time', but this quickly breaks down under examples. We can build incredibly complicated types using Haskell's higher-order functions feature. We also ignore functions that bypass the type system like unsafeCoerce#. These have an extremely important role, but we will consider them separately in due time. A quick note before we begin: for these introductory paragraphs, we ignore the existence of expressions like error and undefined whose denotational semantics are ⊥. This seems extremely weird at first: what do types have to do with theorems? However, as we shall see, the two are very closely related. The Curry–Howard isomorphism, hereafter referred to as simply CH, tells us that in order to prove any mathematical theorem, all we have to do is construct a certain type which reflects the nature of that theorem, then find a value that has that type. The Curry–Howard isomorphism is a striking relationship connecting two seemingly unrelated areas of mathematics - type theory and structural logic.
0 kommentar(er)
