如何提供输入到射型功能

在我的申请，我建立一个类型为一些参数d的（射）函数的表达式。例如：如何提供输入到射型功能

op :: Proxy d -> Proxy ('S d) 
op _ = Proxy 

foo :: forall d . Proxy ('S ('S d)) 
foo = op $ op Proxy

我已经建立了类似foo的表达之后，我想解释它：

getValue :: Proxy (d :: Nat) -> Int 
getValue _ = ...

为了解释foo，我可以打电话给getValue $ foo @'Z，使用类型的应用程序的语法。这很好，除了我的意图是始终用这种模式呼叫getValue。因此，而不是使用户总是要明确他们的表达是相对于'Z，我更喜欢它，如果这个属性是不是固有getValue，让我可以写getValue foo和大概会回来2。

注：一种解决方案是使输入功能输入明确了Proxy：foo :: Proxy d -> Proxy ('S ('S d))和getValue :: (Proxy d1 -> Proxy d2) -> Int，然后有getValue应用功能'Z。这达到了我想要的，但额外的Proxy是烦人的。有没有办法不需要额外的Proxy？

来源

2017-04-04 crockeea

只是好奇：为什么不使用单身？ – Alec

我已经用我的身边'Nat'值的包装单身，所以它会是一点也不麻烦，如果你要提出建议的方法。 – crockeea

问题是'代理::代理t'，但你要'_Z ::代理“Z' - 所以只是定义了这样一个恒定的自己。如果你真的必须将这个工作移动到'getValue'，那么你可以使用实例重叠实例化“自由”类型的变量到''Z'，但它真的不值得。 – user2407038

-2

将您的getValue重命名为getValue'并编写getValue foo = getValue' $ foo @'Z。

getValue :: (forall (d :: Nat). Proxy d) -> Int 
getValue foo = getValue' $ foo @'Z 

getValue' :: Proxy (d :: Nat) -> Int 
getValue' Proxy = ...

这里有一个更好的方式来具体化的自然数，如果这是你的最终目标：

class ReifyNat (n :: Nat) where 
    reifyNat :: Integer 

instance ReifyNat 'Z where 
    reifyNat = 0 

instance ReifyNat n => ReifyNat ('S n) where 
    reifyNat = succ (reifyNat @n) 

getValue :: forall n. ReifyNat n => Proxy n -> Integer 
getValue _ = reifyNat @n

或者只是使用：

getValue :: forall n. ReifyNat n => Integer 
getValue = reifyNat

你或许可以摆脱所有您如果你愿意的话，以这种方式使用Proxy。

来源

2017-04-04 20:19:00 Lazersmoke

我想你的第一行不可能工作，可以吗？我们必须告诉编译器'getValue'的参数可以采用类型应用程序。你的'getValue'的类型是什么？ – crockeea

这里的要点并不是要反映Nat的价值（这只是一个例子）。关键是在调用'getValue'时自动向类型函数提供一个输入。如果它真的编译，你的第一种方法就可以做到这一点。 – crockeea

@crockeea你的问题似乎是更一般的“如何使'f x y'总是使用某些特定的'y'而不是将它作为参数吗？答案是做一个函数'f'x = f x someFixedY'。你可能需要添加一个明确的'forall'：'getValue':: forall（n :: Nat）。 Int'。您只需将类型参数从值级别代理lambda移动到类型级别大写lambda。 – Lazersmoke

如何提供输入到射型功能

回答

相关问题