Idris中Type上的模式匹配 [英] Pattern matching on Type in Idris

问题描述

可能是基本的，但我不明白为什么以下功能为 fnc Nat 和 fnc Integer 回答1，甚至没有包含在模式中

Probably it's elementary but I don't understand why the following function answers 1 for fnc Nat and also, for fnc Integer, which is not even included as a pattern.

fnc : Type -> Integer
fnc Bool = 1
fnc Nat = 2

推荐答案

您不能对类型进行模式匹配，也不应.当我编译您的代码时，我会收到下一个错误:

You can't pattern match on type and you shouldn't. When I compile your code I receive next error:

warning - Unreachable case: fnc Nat

这已经在前面讨论过了:

This was already discussed earlier:

1. 旧讨论.
2. 一些类似的问题.
3. 在GitHub上有一些类似的问题.

1. Old discussion.
2. Some similar question.
3. Some similar issue on GitHub.

更新:

最后找到与答案相关的更重要的问题:

Finally found more relevant question with answer:

为什么输入大小写是一件坏事?

这篇关于Idris中Type上的模式匹配的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！