在 Idris 中键入函数别名答案

【问题标题】：Type Function Aliases in Idris在 Idris 中键入函数别名
【发布时间】：2020-07-01 08:41:22
【问题描述】：

是否可以在 Idris 中定义类型函数的短别名？

在进行以下代码类型检查时，我希望对 AugentRow 有一个更短的定义。

import Data.Vect

ColumnCount : Type
ColumnCount = Nat

Cell : Type
Cell = Type

Row : ColumnCount -> Cell -> Type
Row   columnCount    cell =  Vect columnCount cell

AugentRow : ColumnCount -> Cell -> Type
AugentRow   columnCount    cell =  Row columnCount cell

一些没有像这样不必要重复的定义：

AugentRow = Row

【问题讨论】：

标签： idris

【解决方案1】：

迄今为止我发现的最短形式：

AugentRow : ColumnCount -> Cell -> Type
AugentRow = Row

【讨论】：

这是我遇到过的最短的，虽然我通常发现很难在有多个名称用于完全相同的类型的代码库中工作