如何在Agda中实现类似Haskell的长代码行拆分

Agda默认的布局规则确实比Haskell严格，你遇到的对齐要求是默认布局解析器的特性：->作为中缀运算符，换行后的内容默认需要对齐到->右侧才会被识别为同一表达式的组成部分。你可以通过以下几种方式实现更灵活的长行拆分：

方案1：调整块级缩进（最常用，无额外依赖） #

把postulate关键字单独放在一行，后续所有声明统一缩进固定层级（比如2/4空格），此时类型签名换行只要保持和声明同层级或更深的缩进即可，不需要对齐到->：

postulate
  flipH/cw/cw/flipH : ∀ (t : Tile) ->
    flipH (cw (cw (flipH t))) ≡ cw (cw t)

甚至可以进一步拆分forall部分：

postulate
  flipH/cw/cw/flipH
    : ∀ (t : Tile)
    -> flipH (cw (cw (flipH t))) ≡ cw (cw t)

方案2：用括号包裹类型表达式 #

如果不想调整外层块结构，可以用括号把整个类型包起来，括号内的内容不受默认布局规则限制：

postulate flipH/cw/cw/flipH : (
    ∀ (t : Tile) ->
    flipH (cw (cw (flipH t))) ≡ cw (cw t)
  )

方案3：开启宽松布局选项 #

Agda 2.6.1及以上版本支持--relaxed-layout编译选项，开启后布局规则会和Haskell高度接近，仅要求后续行缩进大于当前块的起始缩进即可，无需严格对齐到特定符号位置。你可以在文件头部添加选项声明：

{-# OPTIONS --relaxed-layout #-}

开启后你之前尝试的两种换行写法都可以正常通过编译。

内容的提问来源于stack exchange，提问作者Farzad Bekran