小编Joh*_*iao的帖子

我正在阅读伊德里斯教程。而且我无法理解下面的代码。

disjoint : (n : Nat) -> Z = S n -> Void
disjoint n p = replace {P = disjointTy} p ()
  where
    disjointTy : Nat -> Type
    disjointTy Z = () 
    disjointTy (S k) = Void

到目前为止，我发现......是 Void空类型，用于证明某些事情是不可能的。

替换：(x = y) -> P x -> P y 替换使用等式证明来转换谓词。

我的问题是：

1. 哪一个是平等证明？(Z = S n)？

2. 哪一个是谓词？功能disjointTy？

3. 目的是什么disjointTy？disjointTy Z = () 是否意味着 Z 位于一个类型“land”() 中且 (S k) 位于另一块土地中Void？

4. Void 输出以什么方式表示矛盾？

诗。我所知道的证明是“凡事不匹配则为假”。或者“找到一件矛盾的事情”......

函数式编程课程练习中FileIO.hs中的一行

getFile :: FilePath -> IO (FilePath, Chars)
getFile = lift2 (<$>) (,) readFile

根据其类型签名，getFile返回IO ( FilePath, Chars)，这意味着文件名及其内容的元组。

但我就是不明白为什么它会变成那样。

为什么FilePath左边是不变的，右边是readFilefilename？

是(,)一个应用型的实例吗？(,)不是IO，那么lift2提升了什么呢？

而且，有没有办法导出这些类型签名并得到证明？

我知道的语法是，一个函数后面跟着它的参数，它吃掉它右手边的一个参数，变成一个新函数。但是当涉及到这样的代码时，对我来说它就像一个魔方......

谢谢你帮我解决！

附言。额外信息如下

instance Functor IO where
  (<$>) =
    P.fmap

lift2 ::
  Applicative f =>
  (a -> b -> c)
  -> f a
  -> f b
  -> f c
lift2 f a b =
  f <$> a <*> b

getFiles …