[prev in list] [next in list] [prev in thread] [next in thread] 

List:       haskell-cafe
Subject:    Re: [Haskell-cafe] Instantiation problem
From:       Tom Nielsen <tanielsen () gmail ! com>
Date:       2011-01-31 10:09:09
Message-ID: AANLkTinDQeZiCNTgX4qo8PNiY+jO=yhaazOWxQSzEKtr () mail ! gmail ! com
[Download RAW message or body]

Patrick,

I find Andrew Frank's work on axiomatic specifications of GIS systems
-- which the paper you cite is built on -- very confusing, or indeed,
confused. They have a bunch of example like

data Car = Car Color

class Car a where
   carColor :: a -> Color

instance Car Car where
   carColor (Car c _) = c

as if there is some kind of special logical interpretation of having a
class Car in addition to the data type Car. As far as I remember, they
interpret type classes as axioms. After reading it, without being an
expert in either GIS or a logician, I came away thinking that they
were mixing some very abstract ideas from object-oriented languages
into Haskell. I find the presentations of type classes by e.g. Mark
Jones, and the links between functional programming and logic from
either the Curry-Howard correspondence or HOL-style reasoning (for
instance, see the HOL light manual), somewhat crisper.

Tom

On Sun, Jan 30, 2011 at 10:27 AM, Patrick Browne <patrick.browne@dit.ie> wrote:
> On 29/01/2011 20:56, Henning Thielemann wrote:
> > Is there a reason why you use an individual type for every unit?
> > The existing implementations of typed physical units only encode the
> > physical dimension in types and leave the unit factors to the value
> > level. I found this to be the most natural way.
> 
> I am studying type classes using examples from the literature [1].
> There is no particular intension to implement anything.
> 
> I am confused about the unit function in the code below.
> My understanding is:
> The signature of the unit function is defined in the MetricDescription
> class.
> Any valid instantce of MetricDescription will respect the functional
> dependency (FD):
> The FD | description -> unit  is exactly the signature of the unit function.
> 
> My confusions
> I do not understand the definitions of unit in the instances.
> I do not know how the constant 1 can be equated with a *type*, Where did
> 1 come from?
> I do not know how the constant 1 can be equated with *two distinct*
> definitions of the function uint and still produce the following correct
> results
> 
> Ok, modules loaded: A.
> *A>  unit (LengthInMetres  7)
> Metre
> *A> unit (LengthInCentimetres 7)
> Centimetre
> *A>
> 
> 
> 
> [1] http://ifgi.uni-muenster.de/~lutzm/odbase04_schade_et_al.pdf
> 
> ======================================================================
> 
> module A where
> 
> -- Each member of the Unit class has one operator convertFactorToBaseUnit
> -- that takes a measurement unit (say metre) and returns a conversion
> factor for that unit of measurement
> class  Unit unit where
> convertFactorToBaseUnit :: unit -> Double
> 
> 
> 
> class (Unit unit) => MetricDescription description unit | description ->
> unit where
> unit :: description -> unit
> valueInUnit :: description -> Double
> valueInBaseUnit :: description -> Double
> valueInBaseUnit d = (convertFactorToBaseUnit(unit d)) * (valueInUnit d)
> 
> data Dog = Dog  deriving Show
> data Metre = Metre  deriving Show
> data Centimetre = Centimetre deriving Show
> 
> 
> -- An instance for metres, where the convert factor is 1.0
> instance Unit Metre where
> convertFactorToBaseUnit Metre  = 1.0
> 
> -- An instance for centimetres, where the convert factor is 0.1
> instance Unit Centimetre where
> convertFactorToBaseUnit Centimetre  = 0.1
> 
> 
> 
> data LengthInMetres = LengthInMetres Double  deriving Show
> data LengthInCentimetres = LengthInCentimetres Double  deriving Show
> 
> instance MetricDescription LengthInMetres Metre where
> valueInUnit (LengthInMetres d) = d
> unit l = Metre
> 
> 
> 
> instance MetricDescription LengthInCentimetres Centimetre where
> valueInUnit (LengthInCentimetres d) = d
> unit l = Centimetre
> 
> 
> 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 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[prev in list] [next in list] [prev in thread] [next in thread]