对于足够多态的类型,参数可以唯一地确定函数本身(有关详细信息,请参阅Wadler的定理免费!).例如,唯一具有类型的总函数forall t. t -> t是标识函数id.
是否有可能在伊德里斯陈述并证明这一点？(如果在伊德里斯内部无法证明,无论如何都是真的吗？)
以下是我的尝试(我知道函数相等不是Idris中的原始概念,所以我断言泛型类型的任何函数t -> t总是返回与身份函数返回的结果相同的结果):
%default total
GenericEndomorphism: Type
GenericEndomorphism = (t: Type) -> (t -> t)
id_is_an_example : GenericEndomorphism
id_is_an_example t = id
id_is_the_only_example : (f : GenericEndomorphism) -> (t : Type) -> (x : t) -> f t x = x
id_is_the_only_example f t x = ?id_is_the_only_example_rhs
由此产生的洞是:
- + Main.id_is_the_only_example_rhs [P]
`-- f : GenericEndomorphism
t : Type
x : t
-------------------------------------------------------
Main.id_is_the_only_example_rhs : …问题是默认处理程序是在Sinatra :: ShowExceptions中定义的,它由:raise_errors配置设置控制,此设置全部或全部.如果:raise_errors已关闭,则可以在Sinatra应用程序中使用error方法,但必须将其用于所有异常,并且无法访问Sinatra :: ShowExceptions中定义的错误处理程序.如果它处于打开状态,则ShowExceptions中间件将处理所有异常.
我想要做的理由是,至少在开发过程中,我希望以用户友好的方式处理"预期"错误,并且我希望以开发人员友好的方式处理"意外"错误.
我猜这样做的唯一方法是定义一个继承自Sinatra :: ShowExceptions的机架中间件类,它在其use方法中有一些额外的选项来指定要处理或不处理的异常类.
有什么比我更容易丢失的方法吗？
(我正在使用jruby,如果这有任何区别.)
在下文中,example1是标准语法(如文档所述),Eq a作为约束.在example2,我Eq a直接指定为参数的类型,编译器接受它.但是,我不清楚我可以指定哪种类型的值.对于特定类型a,例如Nat,我假设以某种方式指定Eq Nat默认实现或某些其他命名实现的实现是有意义的.
%default total
example1: Eq a => (x : a) -> (y : a) -> Type
example1 {a} x y = ?example1_rhs
example1b: Eq a => (x : a) -> (y : a) -> Type
example1b {a} x y = x == y = True
example2: (a : Type) -> Eq a -> (x : a) -> (y : a) -> Type
example2 …