将测量单位类型提升到特定功率

ebb*_*ebb 8 f#

有可能以某种方式为度量类型创建一个pow函数吗?f#中的pow函数仅int作为参数,然后Math类中的pow函数需要float- 但是剂量允许float<cm>.

我首先想到的是:

let rec myPow(x:float<cm>,y:int) =
    if y = 0 then x
    else myPow(x*x, y - 1)
Run Code Online (Sandbox Code Playgroud)

可能会解决,但显而易见的是,每次遇到else线时都会改变返回类型.

有什么建议?

Ank*_*kur 7

我不认为这是可能的.您要求功能返回<cm^2>,以防电源为2,<cm^3>如果是3,依此类推.这使得函数基于计算返回不同的"类型",这在静态类型和类型安全语言中显然是不可能的.不幸的是,我认为衡量单位不能成为"仿制药"以试图进一步发展.

您的函数只能有一个静态返回类型.


Tom*_*cek 6

Ankur是正确的 - 你不能这样做(没有诉诸破坏单位的黑客).

也许更清楚的问题描述是pow函数的类型取决于参数的值,而F#不允许你这样做.你可以想象,如果只使用文字作为第二个参数,这将起作用,但如果使用表达式,它会变得棘手:

pow a 3 // Assuming a = 1.0<cm>, the return type is float<cm ^ 3>
pow a n // Assuming a = 1.0<cm>, the return type is float<cm ^ n>
Run Code Online (Sandbox Code Playgroud)

在第二种情况下,值n必须出现在类型中!

你可以使用一些讨厌的技巧(受这篇Haskell文章的启发),但它变得有点疯狂.除了使用数字文本,你就应该使用类似S(S(S(N)))表示该数字3.这样,您可以将数字带入类型中.你可能不想这样做,但这是一个例子:

[<Measure>] type cm

// Represents a number with units of measure powered to the
// number's value (e.g "(S (S O))" has type Num<cm, cm^3>)
type Num<[<Measure>] 'M, [<Measure>] 'N> = 
  | O_ of int * float<'N>
  | S_ of int * Num<'M, 'N / 'M>

// Constructors that hide that simplify the creation  
let O : Num<'M, 'M> = O_ (1, 0.0<_>)
let S n = match n with O_(i, _) | S_(i, _) -> S_(i + 1, n)

// Type-safe power function with units of measure
let pow (x:float<'M>) ((O_(i, _) | S_(i, _)):Num<'M, 'M 'N>) : float<'M 'N> =
  // Unsafe hacky implementation, which is hidden
  // from the user (for simplicity)
  unbox ((float x) ** float i)

let res = pow 2.0<cm> (S (S O))
Run Code Online (Sandbox Code Playgroud)

编辑:我将源代码发布到F#snippets,以便您可以看到推断类型:http://fssnip.net/4H


Lau*_*ent 5

正如所说,你不能。如果y在编译时未知,则无法在 F# 类型系统中对表达式进行类型检查。

我怀疑您只会将 myPow 与一些小的已知常量一起使用。在这种情况下,您可以使用以下函数并保持静态类型:

let inline pow2 (x: float<'a>) : float<'a^2> = pown (float x) 2 * 1.<_>
let inline pow3 (x: float<'a>) : float<'a^3> = pown (float x) 3 * 1.<_>
let inline pow4 (x: float<'a>) : float<'a^4> = pown (float x) 4 * 1.<_>
let inline pow5 (x: float<'a>) : float<'a^5> = pown (float x) 5 * 1.<_>
Run Code Online (Sandbox Code Playgroud)