前导单引号是啥意思？

Posted 2023-03-24

【中文标题】前导单引号是啥意思？

【英文标题】：What does a leading single quote mean?前导单引号是什么意思？

【发布时间】：2017-07-23 02:39:44

【问题描述】：

前面有' 字符的名称是Type 类型：

Idris> 'foo
'foo : Type

这是什么意思？'foo 类型的值的示例是什么？

【参考方案1】：

字符串值前面的前导单引号将该字符串转换为类型。它是prelude/Builtins.idr中定义的内置语法扩展

||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
data Symbol_ : String -> Type where

如果我理解正确，符号没有值，而仅存在于类型级别。

idris 文档中记录了符号的一个用例：http://docs.idris-lang.org/en/latest/effects/state.html?highlight=symbol，其中符号用于标记具有其他相同类型签名的状态。