命名实现到默认实现
命名实现到默认实现
提问于 2016-05-18 05:41:08
我为Int类型的type typeclass定义了一个命名实现。
[mijnOrd] Ord Int where
compare n1 n2 = ...如何导入这个命名的实现并将其用作“默认”
- 因此，在另一个模块中，我想导入这个实现
- 将其标记为默认
- 并将其当作默认使用。
--
sort [1,5,2] -- output without importing as default: [1,2,5]
sort [1,5,2] -- output with importing as default: [5,2,1]这在伊德里斯有可能吗？
回答 1
Stack Overflow用户
回答已采纳
发布于 2016-07-14 23:49:01
这是可能的，因为Idris 0.12使用using-blocks：
在一个模块中导出指定的接口，比如MyOrd.idr
module MyOrd
-- Reverse order for `Nat`
export
[myOrd] Ord Nat where
compare Z Z = EQ
compare Z (S k) = GT
compare (S k) Z = LT
compare (S k) (S j) = compare @{myOrd} k j然后，只需将其导入另一个模块中，并在相应的using-block中包装所有应该将其作为默认值使用的内容，如下所示：
-- Main.idr
module Main
import MyOrd
using implementation myOrd
test : List Nat -> List Nat
test = sort
main : IO ()
main = putStrLn $ show $ test [3, 1, 2]这应该会打印[3, 2, 1]。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/37301403
复制相关文章
点击加载更多
相似问题
统一阴影在编辑器中工作，而在构建中不工作。
为什么valign=“底部”不能在火狐中工作，而在IE和Chrome中工作呢？
为什么我的UI Button在构建后在编辑器中工作，而在android中不工作呢？
为什么我的RegEx在PHP中工作，而在JavaScript中不工作呢？
为什么font-lock-fontify-buffer不能在elisp中工作，而在minibuffer中工作呢？
添加站长 进交流群
领取专属 10元无门槛券
AI混元助手 在线答疑
关注 腾讯云开发者公众号
洞察 腾讯核心技术
剖析业界实践案例
腾讯云开发者
