小编Typ*_*ats的帖子

我注意到 Cubical 标准库定义Fin为依赖对而不是索引归纳类型。原因是 Cubical Agda 不完全支持索引归纳类型：https : //github.com/agda/cubical/pull/104#discussion_r268476220

一个链接问题指出模式匹配不适用于归纳家庭，因为hcomp并且transp尚未对其进行定义：https : //github.com/agda/cubical/pull/57#issuecomment-461174095

我定义Fin并Vec编写了一个模式匹配函数，它似乎工作正常：

{-# OPTIONS --cubical --safe #-}

open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat using (?; zero; suc)

private
  variable
    ? : Level
    A : Type ?
    n : ?

data Fin : ? ? Type? where
  fzero : Fin (suc n)
  fsuc : Fin n ? Fin (suc n)

data Vec (A : Type ?) : ? ? …

我正在Agda中尝试同伦类型理论。我使用HIT定义整数：

{-# OPTIONS --cubical --safe #-}

open import Cubical.Foundations.Prelude
open import Data.Nat using (?; _+_)

data ? : Set where
  -- | An integer i is a pair of natural numbers (m, n)
  --   where i = m - n
  int : ? ? ? ? ?
  -- | (a, b) = (c, d)
  --   a - b = c - d
  --   a + d = b + c
  int-eq : ? {a b c d : ?} ? …

OCaml值通过引用传递,而不是通过值传递.当值恒定时,引用和值之间没有可观察到的差异.但是,当值是可变的时(例如具有可变字段的结构),我可能想要复制它,以便当一个变量改变该值时,另一个设置为前一个变量的变量也不会发生变异.我可以在OCaml中这样做吗？

我在OCaml中创建monad并需要编写它们,所以我创建了变换器.我使用Identity monad在变换器方面实现了常规monad:

module type MONAD = sig
  type 'a m
  val (>>=) : 'a m -> ('a -> 'b m) -> 'b m
  val return : 'a -> 'a m
end

module Identity : MONAD = struct
  type 'a m = 'a
  let (>>=) m f = f m
  let return x = x
end

module OptionT (M : MONAD) : MONAD with type 'a m := ('a option) M.m = struct
  type 'a m = ('a option) M.m
  let …