标签: parametric-polymorphism

对Haskell来说是非常新的知识，它试图了解类型类和变量如何交互。

我要玩的第一件事是：

i :: a; i = 1

我的期望是，由于我输入的字词尽可能通用，因此我应该绝对可以为其分配任何内容。（我知道我可能无法对变量i做任何事情，但这并不重要。）

但是我错了。上面给出了一个错误，并要求它是：

i :: Num a => a; i = 1

经过多玩之后，我想到了以下内容：

g :: Num a => a -> a; g a = a + 1
g 1
(returned 2)
gg :: Num a => a; gg = g 1
gg
(returned 2)

好的...到目前为止很好。让我们尝试一个小数参数。

g :: Num a => a -> a; g a = a + 1
g 1.3
(returned 2.3)
gg :: Num a => a; gg = g 1.3 …

从MSDN文档中,签名List.max是:

List.max : 'T list -> 'T (requires comparison)

我的问题是:

• 编译器如何静态验证是否'T支持比较操作？
• 是requires指定类型约束的关键字吗？如果是,我可以指定所有类型的约束吗？
• 我可以定义自己的约束,就像我可以在Scala中使用类型类一样吗？

我想计算我的功能,其中一些最多使用三个参数.现在我正在使用下面相同的代码,其中包含三种变体.

let GetTime f (args : string) = 
    let sw = Stopwatch.StartNew()
    f (args)
    printfn "%s : %A" sw.Elapsed 

我想用这个替换三个函数.

let GetTime f ( args : 'T[]) =
    let sW = Stopwatch.StartNew()
    match args.Length with
    | 1 -> f args.[0]
    | 2 -> f (args.[0] args.[1])
    printfn "%A" sW.Elapsed
    ()

但是如果我使用它运行的三个函数,我会收到类型不匹配的错误.是否可以将函数作为参数发送并像这样使用它？

为了我自己的理解,我想在Haskell中定义一个带有两个参数的函数 - 无论是整数还是两个Chars.它对参数做了一些微不足道的检查,如下:

foo 1 2 = 1
foo 2 1 = 0
foo 'a' 'b' = -1
foo _ _ = -10

我知道这不会编译,因为它不知道它的args是Num还是Char类型.但我无法使其论证具有多态性,例如:

foo :: a -> a -> Int

因为那时我们说它必须是身体中的Char(或Int).

是否可以在Haskell中执行此操作？我想过可能会创建一个自定义类型？就像是:

data Bar = Int | Char
foo :: Bar -> Bar -> Int

但我认为这也不合适.一般来说,我很困惑Haskell中的函数是明确的ONE类型,还是类型类的多态,是否禁止在函数体中使用特定类型.

在Haskell中有可能有一个可以采用多态类型并返回多态类型的函数吗？

例如,我想要一个接受值的函数,如果值是类型则返回一个Int,如果是类型则返回Foo一个StringBar

data Foo = One | Two | Three deriving (Show, Read)
data Bar = This | That | TheOther deriving (Show, Read)

doSomething :: Either Foo Bar -> Either Int String
doSomething var = if (typeOf var) == Int then 123 else "string"

这样的事情可能吗？如果没有,基于类型路由到另一个函数的最佳实践是什么？

阅读这个答案促使我尝试构建,然后证明多态容器函数的规范形式.施工很简单,但证据证明了这一点.下面是我尝试编写证明的简化版本.

简化版本证明,由于参数性,足够多态的函数不能仅基于参数的选择来改变它们的行为.假设我们有两个参数的函数,一个是固定类型,另一个是参数:

PolyFun : Set ? Set _
PolyFun A = ? {X : Set} ? A ? X ? A

我要证明的财产:

open import Relation.Binary.PropositionalEquality

parametricity : ? {A X Y} ? (f : PolyFun A) ? ? a x y ? f {X} a x ? f {Y} a y
parametricity f a x y = {!!}

这样的陈述是否可以从Agda内部证明？

功能:

fn : 'a -> 'b

现在,是否有任何可以定义并具有此类型的功能？

The Elm docs illustrate type variables like this:

> List.reverse
<function> : List a -> List a

...the type variable a can vary depending on how List.reverse is used. But in this case, we have an a in the argument and in the result. This means that if you give a List Int you must get a List Int as well.

The docs for Maybe.map show this annotation:

map : (a -> b) -> Maybe a -> Maybe b

那么为什么这些类型被注释为 …

我有一个函数f op = (op 1 2, op 1.0 2.0)，它需要像这样工作：

f (+)
(3, 3.0)

但是没有声明f它的类型是这样的：

f (+)
(3.0, 3.0)

我正在努力声明f. 它应该采用一个与Num. 在 Haskell 中甚至有可能吗？

在使用cubical-agda进行一些开发期间，我注意到（后来检查）我当前的目标如果被证明也意味着这样的定理：

parametric? : \xe2\x88\x80 \xe2\x84\x93 \xe2\x86\x92  Type (\xe2\x84\x93-suc \xe2\x84\x93)  \nparametric? \xe2\x84\x93 = (f : {A : Type \xe2\x84\x93} \xe2\x86\x92 List A \xe2\x89\x83 List A)\n                   \xe2\x86\x92 (A : Type \xe2\x84\x93) \xe2\x86\x92 length \xe2\x88\x98 equivFun (f {A}) \xe2\x89\xa1 length\n

我怀疑这是参数定理的例子，这是正确的，但在三次 agda 中无法证明。是这样吗？

我可以放心地假设我当前的目标也是无法证明的吗？