Haskell中简单的从属类型的温度转换器，是否可以缩短代码长度？ [英] Simple dependently typed Temperature converter in Haskell, is it possible to make this code shorter?

问题描述

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

SUnit fromUnit-> ; SUnit toUnit - >值fromUnit - > Value toUnit ，

其中冗余，因为相同的信息可以表示为：

来自Unit的值 - >价值单位。

<1>有没有办法摆脱前两个参数（ SUnit fromUnit-> SUnit toUnit ）？
$ b $ 2）有没有其他的方式可以更简单地编写这个简单的依赖类型的程序？

$ b p> 3）这个程序在Idris中看起来如何？

  { - ＃LANGUAGE GADTs，DataKinds，KindSignatures＃ - } 
 main = do 
 putStrLnHello！ 
  -  putStrLn $ show $ convert SCelsius SCelsius kelvinZero  - 这一行不会编译
 putStrLn $ show $ convert SKelvin SKelvin kelvinZero  - 输出值0.0 
 putStrLn $ show $ convert SKelvin SCelsius kelvinZero - 打印值（-273.16）
 
新类型值（单位::单位）=值双重派生显示
数据单位=摄氏度| Kelvin 
 
数据SUnit u其中
 SCelsius :: SUnit摄氏度
 SKelvin :: SUnit开尔文
 
抵消= 273.16 
 convert :: SUnit fromUnit-> SUnit toUnit  - >值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-抵消
转换SKelvin SKelvin（Value tempK）=价值$ tempK 
 
 kelvinZero：:(价值'开尔文）
 kelvinZero =价值0 
  
 
 
解决方案
如果你想删除前两个参数，在Haskell中你需要一个类型类。
  class IsUnit a其中
 getSUnit :: SUnit a 
实例IsUnit Celsius其中getSUnit = SCelsius 
实例IsUnit Kelvin where getSUnit = SKelvin 
 
 convertShort ::（IsUnit fromUnit，IsUnit toUnit）=>来自单位的价值 - > Value toUnit 
 convertShort =转换getSUnit getSUnit 
  
请注意，这会使代码更长，而不是更短 - 但它允许调用者忽略第一个单例值。
 
 
上面的代码还假设每个单位都可以转换为任何其他单位，这是不现实的。原始代码也包含这个问题。如果不需要，可以使用两个参数类型的类： 
 
 
  class C from to convert convert :: Value from - >价值到
实例C Kelvin Celsius其中... 
  - 等
  
 
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

解决方案
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.


                        
这篇关于Haskell中简单的从属类型的温度转换器，是否可以缩短代码长度？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！