如何解决接口:参数化值还是使用更高的友好度?
我试图弄清楚这三个界面之间的区别,以及何时使用每个界面
interface Foo (xs : List Nat) (n : Nat) bar where
...
interface Foo' (xs : List Nat) (bar : Nat -> Type) where
...
interface Foo'' (bar : List Nat -> Nat -> Type) where
...
我认为它类似于 Functor
vs Show
,但我对此也有点含糊。有什么想法吗?
背景
我目前使用 Foo'
,并且我在类型别名中使用它
Baz : Foo' xs bar => Type
Baz {bar} = forall m . Vect m Double -> bar m
但是在使用站点我需要指定 xs
两次:Baz {xs=[1]} {bar=MyFoo [1]}
用于某些 Foo' xs (MyFoo' xs) where
,我不太明白,因为只有一个可能的值可以用于 {{ 1}} 在 xs
的应用中。我正在探索其他的,看看它们是否有效(还没有成功),但我不太清楚每个 API 的含义是什么。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。