DPair 在 Fin 上索引

Question

我正在学习 Idris 教程并想进行实验有依赖对和 Fin.

以下代码不会在 Idris 中进行类型检查。

data Fin : Nat -> Type where
    FZ : Fin (S k)
    FS : Fin k -> Fin (S k)

P : (Fin 1) -> Type 
P FZ = Char 

vec : DPair (Fin 1)  P 
vec = MkDPair FZ 'c'

错误如下

prims.idr:9:15:
When checking right hand side of vec with expected type
        DPair (Fin 1) P

When checking argument pf to constructor Builtins.MkDPair:
    Type mismatch between
            Char (Type of 'c')
    and
            P FZ (Expected type)

我已经检查过 P FZ 是 Char，所以我对类型不匹配投诉感到困惑。使用 Nat 代替 Fin 1 编译的相应代码完美。我做错了什么？

Answer 1

P FZ 没有规范化为 Char，因为编译器看不到 P 是总的（使用 %default total 得到警告）。这有效：

data Fin : Nat -> Type where
    FZ : Fin (S k)
    FS : Fin k -> Fin (S k)

P : (Fin 1) -> Type 
P FZ = Char 
P (FS FZ) impossible
P (FS (FS _)) impossible

vec : DPair (Fin 1)  P 
vec = MkDPair FZ 'c'

DPair 在 Fin 上索引

DPair indexed over Fin

functional-programming

idris