Simple dependently typed Temperature converter in

问题:

The function convert below has the type signature :

SUnit fromUnit-> SUnit toUnit ->Value fromUnit -> Value toUnit,

which has redundancy, because the same information could be expressed by :

Value fromUnit -> Value toUnit.

1) Is there a way to get rid of the first two arguments (SUnit fromUnit-> SUnit toUnit) ?

2) Is there some other way by which this simple dependently typed program could be written more elegantly ?

3) How would this program look like in Idris ?

{-# LANGUAGE GADTs,DataKinds,KindSignatures #-}
main=do
    putStrLn "Hello !"
--  putStrLn $ show $ convert SCelsius  SCelsius kelvinZero -- this line does not compile
    putStrLn $ show $ convert SKelvin SKelvin  kelvinZero -- prints Value 0.0
    putStrLn $ show $ convert SKelvin SCelsius kelvinZero -- prints Value (-273.16)

newtype Value (unit::Unit) = Value Double deriving Show
data Unit = Celsius | Kelvin

data SUnit u where
  SCelsius:: SUnit Celsius
  SKelvin::  SUnit Kelvin

offset=273.16
convert :: SUnit fromUnit-> SUnit toUnit ->Value fromUnit -> Value toUnit
convert          SCelsius         SKelvin  (Value tempCel) = Value $tempCel+offset
convert          SCelsius         SCelsius (Value tempCel) = Value $tempCel
convert          SKelvin          SCelsius (Value tempK)   = Value $tempK-offset
convert          SKelvin          SKelvin  (Value tempK)   = Value $tempK

kelvinZero::(Value 'Kelvin)
kelvinZero= Value 0

回答1:

If you want to remove the first two arguments, in Haskell you need a typeclass.

class IsUnit a where
   getSUnit :: SUnit a
instance IsUnit Celsius where getSUnit = SCelsius
instance IsUnit Kelvin  where getSUnit = SKelvin

convertShort :: (IsUnit fromUnit, IsUnit toUnit) => Value fromUnit -> Value toUnit
convertShort = convert getSUnit getSUnit

Note that this makes the code longer, not shorter -- but it allows the callers to omit the first singleton values.

The above code also assumes that every unit is convertible to any other one, which is unrealistic. The original code also contains this issue. If that is not wanted, one could use a two-parameters type class:

class C from to where convert :: Value from -> Value to
instance C Kelvin Celsius where ...
-- etc.