[Haskell-cafe] logic and types

[Patrick Browne]

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
-- The :type command says
-- forall a. (Pos a) => a -> Position
-- How do I write this in logic? (e.g. implies, and, or, etc)
-- What exactly is being asserted about the type variable and/or about
the class?
-- I am not sure of the respective roles of => and -> in a logical context


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

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

This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie