Безопасные для единицы квадратные корни - PullRequest
Новая
       20

Безопасные для единицы квадратные корни

9 голосов
/ 01 октября 2009

Мне просто интересно, как можно написать пользовательскую функцию квадратного корня (sqrt) таким образом, чтобы она правильно взаимодействовала с F # * модульной системой .

Как это должно быть: 

let sqrt (x : float<'u ^ 2>) =
    let x' = x / 1.0<'u ^ 2> // Delete unit
    (x ** 0.5) * 1.0<'u>     // Reassign unit

Но это запрещено из-за того, что ненулевым константам не разрешено иметь общие единицы .

Есть ли способ написать эту функцию? Со встроенным sqrt он работает нормально, так что же за магию он выполняет?

Ответы [ 2 ]

6 голосов
/ 02 октября 2009

@ kvb верно, в более общем смысле:

Если у вас есть алгоритм, не связанный с единицами (например, вы пишете «корень куба»), и вы хотите поместить в него единицы измерения, вы можете заключить алгоритм в функцию с правильной сигнатурой типа и использовать, например, например. «плавать», чтобы «отбрасывать» отряды по мере их появления, и подход «бокс и падающий», чтобы «добавлять обратно» соответствующие отряды на выходе.

В версии RTM (после Beta2) F # будет иметь примитивные библиотечные функции для «добавления обратно блоков», так как подход box-and-downcast в настоящее время является хаком, чтобы преодолеть недостаток этих примитивов в язык / библиотека.

6 голосов
/ 01 октября 2009

Разрешение ненулевых общих констант может очень легко нарушить безопасность системы типов для единиц (см. документы Эндрю Кеннеди ). Я полагаю, что ответ на ваш последний вопрос заключается в том, что sqrt действительно волшебно в некотором смысле в том смысле, что невозможно определить параметрическую функцию с такой сигнатурой типа обычными средствами. Тем не менее, можно делать, что вы хотите (по крайней мере, в текущей версии F #), используя преимущества бокса и кастинга: 

let sqrt (x : float<'u^2>) =
  let x' = (float x) ** 0.5 (* delete unit and calculate sqrt *)
  ((box x') :?> float<'u>)
...