functor - VerifiedFunctor - 证明映射(映射 g)x = x
问题描述
我试图证明关于VerifiedFunctor
接口的声明(一种尊重身份和组合的方法)Functor
:map
interface Functor f => VerifiedFunctor (f : Type -> Type) where
functorIdentity : {a : Type} -> (g : a -> a) -> ((v : a) -> g v = v) ->
(x : f a) -> map g x = x
这是语句(从逻辑上讲,map . map
对于两个给定的函子也尊重身份):
functorIdentityCompose : (VerifiedFunctor f1, VerifiedFunctor f2) =>
(g : a -> a) -> ((v : a) -> g v = v) ->
(x : f2 (f1 a)) -> map (map g) x = x
functorIdentityCompose fnId prId = functorIdentity (map fnId) (functorIdentity fnId prId)
但是,我收到以下错误:
Type mismatch between
(x : f1 a) -> map fnId x = x (Type of functorIdentity fnId prId)
and
(v : f a) -> map fnId v = v (Expected type)
Specifically:
Type mismatch between
f1 a
and
f a
我试图指定所有隐式参数:
functorIdentityCompose : (VerifiedFunctor f1, VerifiedFunctor f2) =>
{a : Type} -> {f1 : Type -> Type} -> {f2 : Type -> Type} ->
(g : a -> a) -> ((v : a) -> g v = v) -> (x : f2 (f1 a)) ->
map {f=f2} {a=f1 a} {b=f1 a} (map {f=f1} {a=a} {b=a} g) x = x
...但是又出现了一个错误:
When checking argument func to function Prelude.Functor.map:
Can't find implementation for Functor f15
那么有什么想法这里出了什么问题以及如何证明这一说法?
解决方案
这是一个启发式:当“显而易见”的事情不起作用时...... eta-expand!所以这有效:
functorIdentityCompose : (VerifiedFunctor f1, VerifiedFunctor f2) =>
(g : a -> a) -> ((v : a) -> g v = v) ->
(x : f2 (f1 a)) -> map (map g) x = x
functorIdentityCompose fnId prId x =
functorIdentity (map fnId) (\y => functorIdentity fnId prId y) x
看起来完整的应用程序会触发实例搜索。
推荐阅读
- angular - 角度图像缩放悬停效果
- powershell - 从 Json 对象中检索值,其字段在 powershell 中具有点和连字符
- node.js - 快速服务器的 axios 响应中未填充“数据”字段
- javascript - 如何在geoJSON中添加标签和标题到点(标记),一旦加载就会显示在谷歌地图上
- typescript - 带有类型或接口的类型断言
- angular8 - 如何创建按钮作为重置按钮以重置 angular8 中的表单?
- mysql - 使用 EF 和 MySql 在生成的迁移上手动设置注释
- javascript - Jquery .css('背景', '值'); 不工作
- java - TreeSet 如何为添加维护 O(logN)?
- java - 创建无参数方法和字符串参数的区别?