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.