小编Li-*_*Xia的帖子

这两个定义之间有什么区别：

Definition f : forall x:bool, if x then bool else nat :=
  fun x => match x with
           | true => true
           | false => 42
           end.
(* ^ Accepted by Coq *)

Definition g : forall x:bool, if x then bool else nat :=
  fun x => if x then true else 42.
(* ^ REJECTED *)

以前，我以为这if实际上是糖，match但在依赖模式匹配方面似乎更具限制性，即使它也支持return语法。

这是故意的吗？如果是，规则是什么？

动机:能够在Free/ Freer-style中控制MTL中的效果.

这个例子可能有点做作 - 想象一个带有一些基本操作的程序(使用GHC 8.2 freer-simple),

#!/usr/bin/env stack
-- stack --resolver lts-10.2 --install-ghc runghc --package freer-simple
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE LambdaCase #-}
import Control.Monad.Freer

data Effect next where
  ReadFilename :: String -> Effect String
  WriteOutput :: Show a => a -> Effect ()
  Computation :: Int -> Int -> Effect Int

readFilename :: Member Effect effs => String -> Eff effs String
readFilename = send …

假设我有一个代数数据类型Building：

data Building 
  = BRestaurant Restaurant 
  | BStore Store 
  | BHouse House 
  ...

Restaurant, Store, House, ... 都是一些类的实例。现在让我们只使用Show. 我目前将Building的Show实例定义为：

instance Show Building where 
  show (BRestaurant a) = show a
  show (BStore a)      = show a
  show (BHouse a)      = show a
  ...

这似乎非常重复。知道每个元素实例显示并且每个构造函数只有一个参数，有没有办法将 show 函数应用于内部数据？我是否错过了其他可以减少重复的东西？理想情况下，我最终会得到类似的结果：

instance Show Building where 
   show a = applyFunctionMagic show a