我正在尝试在 Idris 中实现最简单的仿函数光学器件。 Iso 是一个在所有代仿函数中都应该是多态的函数。我认为这是正确的语法。
除最终测试外,所有内容均经过类型检查。
interface Profunctor (p : Type -> Type -> Type) where
dimap : (a' -> a) -> (b -> b') -> p a b -> p a' b'
Iso : Type -> Type -> Type -> Type -> Type
Iso a b s t = {p : Type -> Type -> Type} -> Profunctor p => p a b -> p s t
-- A pair of functions
data PairFun : Type -> Type -> Type -> Type -> Type where
MkPair : (s -> a) -> (b -> t) -> PairFun a b s t
-- PairFun a b s t is a Profunctor in s t
Profunctor (PairFun a b) where
dimap f g (MkPair get set) = MkPair (get . f) (g . set)
-- Extract a pair of functions from an Iso
fromIso : Iso a b s t -> PairFun a b s t
fromIso iso = iso (MkPair id id)
-- Turn a pair of functions to an Iso
toIso : PairFun a b s t -> Iso a b s t
toIso (MkPair get set) = dimap get set
-- forall p. Profunctor p => p Int Int -> p Char String
myIso : Iso Int Int Char String
myIso = toIso (MkPair ord show)
x : PairFun Int Int Char String
x = fromIso myIso
我收到此错误。看起来 Idris 正在提示 p1 是 Profunctor 的假设,但这是 Iso 定义中的约束。
Can't find implementation for Profunctor p1
Type mismatch between
p1 Int Int -> p1 Char String (Type of myIso p1
constraint)
and
p Int Int -> p Char String (Expected type)
Specifically:
Type mismatch between
p1 Int Int
and
p Int Int
最佳答案
以下代码在 Idris 2 版本 0.3 中适用于我。这是 Idris 2 的一个相当旧的版本,但它可能也适用于更新的版本。
interface Profunctor (0 p : Type -> Type -> Type) where
dimap : (a' -> a) -> (b -> b') -> p a b -> p a' b'
Iso : Type -> Type -> Type -> Type -> Type
Iso a b s t = {0 p : Type -> Type -> Type} -> Profunctor p => p a b -> p s t
data PairFun : Type -> Type -> Type -> Type -> Type where
MkPair : (s -> a) -> (b -> t) -> PairFun a b s t
Profunctor (PairFun a b) where
dimap f g (MkPair get set) = MkPair (get . f) (g . set)
fromIso : Iso a b s t -> PairFun a b s t
fromIso iso = iso (MkPair id id)
toIso : PairFun a b s t -> Iso a b s t
toIso (MkPair get set) = dimap get set
myIso : Iso Int Int Char String
myIso = toIso (MkPair ord show)
x : PairFun Int Int Char String
x = fromIso myIso
不幸的是,我不知道如何在 Idris 1 中进行这项工作。问题似乎是 p
的生成性。 :阐述者没有推断p1 = p2
来自p1 a b = p2 a b
。在任何 Idrises 中,这通常都不成立,因为 p1
和p2
可以是任意函数。 Idris 2 似乎继续到 p1 = p2
无论如何,在某个时刻;这是一个便利的功能,但代价是一些推理的稳健性。
p
上的不相关注释上面代码中的 与我刚才提到的生成问题无关,它们只是重现 Idris 1 和 GHC 行为所需要的。在 Idris 2 中,隐式引入的变量始终具有 0
多重性,所以我们必须制作 p
也被删除,以便能够将其应用到 0
类型参数。此外,0 p
与 Idris 1/GHC 行为相匹配,其中类型通常被删除。在 Idris 2 中,仅当与 0
绑定(bind)时类型才会被删除.
关于polymorphism - Profunctor Iso 不进行类型检查,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/70178976/