[Haskell-cafe] logic and types

[Ben Lippmeier]

On 01/09/2011, at 8:48 , Patrick Browne wrote:

> Hi,
> Below are some questions about the logical interpretation of types and
> type classes.
> 
> Thanks,
> Pat
> 
> module J where
> type Id = String
> type Position = Integer
> data Person = Person Id Position deriving Show
> 
> -- Is this an axiom at type level?
> class Pos a  where
>   getPos :: a -> Position

One way to think of a type class is that it defines a set of types. For example, Eq is the set of types that support equality, and Pos is the set of types that have a position. By giving the class definition you've defined what it means to be a member of that set, namely that members must support the 'getPos' method, but without instances that set is empty. Whether you treat this bare class definition as an axiom depends on what you want from your logical system. 


> -- The :type command says
> -- forall a. (Pos a) => a -> Position
> -- How do I write this in logic? (e.g. implies, and, or, etc)

Type systems are logical systems, there is no difference. Granted, some systems correspond to parts of others, but there is no single logical system that can be considered to be *the logic*. An equivalent question would be: "how do I write this in functional programming?"


> -- What exactly is being asserted about the type variable and/or about
> the class?

If you ignore the possibility that the function could diverge, then it says "For all types a, given that 'a' is a member of the set Pos, and given a value of type 'a', then we can construct a Position".

Note that this doesn't guarantee that there are any types 'a' that are members of Pos. In Haskell you can define a type class, but not give instances for it, and still write functions using the type class methods.


> -- I am not sure of the respective roles of => and -> in a logical context

Once again, "which logic?". The type system that checks GHC core is itself a logical system. GHC core has recently ben rejigged so that type class constraints are just the types of dictionaries. In this case we have:

 forall (a: *). Pos a -> a -> Position

In DDC core, there are other sorts of constraints besides type class constraints. In early stages of the compiler we encode type class constraints as dependent kinds, so have this:

 forall (a: *). forall (_: Pos a). a -> Position.

Both are good, depending on how you're transforming the core program.


> -- Is the following a fact at type level, class level or both?
> instance Pos Person where
>  getPos (Person i p) = p

If you take the GHC approach, a type class declaration and instance is equivalent to this:

data Pos a 
 = PosDict { getPos :: Pos a -> a -> Position }

dictPosPerson :: Pos Person
dictPosPerson
 = PosDict (\d (Person i p) -> p)

From this we've got two facts:
 Pos :: * -> *
 dictPosPerson :: Pos Person

You could interpret this as:
 1) There is a set of types named Pos
 2) There is an element of this set named Person.


> -- Is it the evaluation or the type checking that provides a proof of
> type correctness?
> -- getPos(Person "1" 2)

The type inferencer constructs a proof that a Haskell source program is well typed. It does this by converting it to GHC core, which is a formal logical system. The core program itself is a proof that there is a program which has its type. The type checker for GHC core then checks that this proof is valid.

Ben.