Простой преобразователь температуры с зависимым типом в Haskell, можно ли сделать этот код короче?

Функция convert ниже имеет сигнатуру типа:

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

который имеет избыточность, поскольку одна и та же информация может быть выражена с помощью:

Value fromUnit -> Value toUnit.

1) Есть ли способ избавиться от первых двух аргументов (SUnit fromUnit-> SUnit toUnit)?

2) Есть ли какой-либо другой способ, с помощью которого можно было бы написать эту простую программу с зависимым типом более элегантно?

3) Как эта программа будет выглядеть в Идрисе?

{-# 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

haskell dependent-type idris
person jhegedus    schedule 03.01.2016    source источник
comment
Ps, для тех, кто задается вопросом, как это можно написать в Идрисе, книга Идриса, глава 3.4.3 Использование неявных аргументов в функциях, кажется, где ответ.   -  person jhegedus    schedule 03.01.2016

Ответы (1)


arrow_upward
4
arrow_downward

Если вы хотите удалить первые два аргумента, в 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.
person chi    schedule 03.01.2016
comment
Это полезно, потому что упрощает код вызывающей стороны. - person jhegedus; 03.01.2016