Haskell中简单的依赖类型温度转换器，是否可以使此代码更短？

Question

下面的函数convert具有类型签名：

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

它具有冗余，因为相同的信息可以表示为：

Value fromUnit -> Value toUnit。

1) 有没有办法摆脱前两个参数 (SUnit fromUnit-> SUnit toUnit) ？

2) 有没有其他方法可以更优雅地编写这个简单的依赖类型程序？

3) 这个程序在 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

Answer 1

如果你想删除前两个参数，在 Haskell 中你需要一个类型类。

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

请注意，这会使代码更长，而不是更短——但它允许调用者省略第一个单例值。

上面的代码还假设每个单位都可以转换为任何其他单位，这是不现实的。原始代码也包含这个问题。如果不想这样，可以使用双参数类型类：

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