小编dor*_*ard的帖子

我正在关注Conor McBride的"Kleisli箭头的令人发指的财富"论文,我在这里发布了我的代码实现.简而言之,他定义了以下类型和类:

type a :-> b = forall i . a i -> b i

class IFunctor f where imap :: (a :-> b) -> (f a :-> f b)

class (IFunctor m) => IMonad m where
    skip :: a :-> m a
    bind :: (a :-> m b) -> (m a :-> m b)

data (a := i) j where
    V :: a -> (a := i) i

然后他定义了两种类型的绑定,后者(:=)用于限制初始索引:

-- Conor McBride's "demonic bind"
(?>=) …

众所周知,实现Haskell类型类的一种方法是通过'类型类词典'.(这当然是ghc中的实现,尽管我强制要求其他实现是可能的.)为了解决这个问题,我将简要介绍一下这是如何工作的.类声明就像

class (MyClass t) where
  test1 :: t -> t -> t
  test2 :: t -> String
  test3 :: t

可以机械地转换为数据类型的定义,如:

data MyClass_ t = MyClass_ {
  test1_ :: t -> t -> t,
  test2_ :: t -> String,
  test3_ :: t,
  }

然后我们可以将每个实例声明机械地转换为该类型的对象; 例如:

instance (MyClass Int) where
  test1 = (+)
  test2 = show
  test3 = 3

变成

instance_MyClass_Int :: MyClass_ Int
instance_MyClass_Int =  MyClass_ (+) show 3

类似地,具有类型类约束的函数可以变成一个带有额外参数的函数; 例如:

my_function :: (MyClass t) => t -> String
my_function …

一段时间以来，我一直在抨击这个问题：我有记录类型，有依赖字段，我想证明记录转换的相等性。我试图将问题的症结提炼成一个小例子。考虑以下记录类型Rec，它在字段之间具有依赖性：

module Bar where
open import Data.Nat
open import Relation.Binary.PropositionalEquality as PE
open import Relation.Binary.HeterogeneousEquality as HE

record Rec : Set where
  field val : ?
        inc : {n : ?} -> ?
        succ : inc {0} ? val

open Rec

该succ属性声明了其他两个字段之间的关系：即inc {0}返回val。以下函数incR定义了一个Rec转换器，该转换器将 value 和 incrementor 增加一个固定值m，这保留了它们的交互：

succPrf : {x : Rec} {m : ?} -> (inc x {0} + m) ? val x + m …

几天来,我一直在反对一个问题,但我的Agda技能不是很强.

我试图在索引数据类型上编写一个函数,该类型仅在特定索引处定义.这仅适用于数据构造函数的某些特化.我无法弄清楚如何定义这样的功能.我试图将我的问题减少到一个较小的例子.

该设置涉及自然数列表,具有用于见证列表成员的类型,以及用于删除列表成员的功能.

open import Data.Nat
open import Relation.Binary.Core

data List : Set where
   nil : List
   _::_ : (x : ?) -> (xs : List) -> List

-- membership within a list
data _?_ (x : ?) : List -> Set where 
   here : forall {xs} -> x ? (x :: xs)
   there : forall {xs y} -> (mem : x ? xs) -> x ? (y :: xs) 

-- delete
_\\_ : forall {x} (xs : List) -> …