时间戳

首页 > 解决方案 > 重新导出实现而不导出定义

module - 重新导出实现而不导出定义

问题描述

假设我有M1一个根据另一个现有类型定义类型的模块：

module M1 

import public Control.Monad.Identity

public export M : Type -> Type
M = Identity

我当然可以在任何期望的地方导入M1和使用：MApplicative

module M2

import M1

bar : M ()
bar = pure ()

但是如果我不想 exportM的定义呢？换句话说，我想写

export M :: Type -> Type
M = Identity

这样客户端代码就不能依赖于M的定义，但我仍然希望客户端代码能够访问Applicative M.

标签： modulepublicidris

解决方案

推荐阅读