如何在不使用Debug.todo的情况下将Elm函数f:A→Maybe B约束为f0:ProperA→B？

核心问题 #

给定函数 f: A -> Maybe B，已定义 isProper : A -> Bool 判断输入是否能让 f 返回 Just 值；同时有包装类型 ProperA，仅能通过 fromA: A -> Maybe ProperA 生成（仅当 isProper 为真时返回 Just）。需实现函数 f0 : ProperA -> B，满足 Just (f0 (ProperA a)) == f a，且不能使用case表达式或Debug.todo，核心目标是通过类型系统排除非法输入，实现"不可能状态不可能"（比如已知字符串非空时安全调用String.uncons）。

具体实现（以Haskell为例） #

利用模块封装隐藏ProperA的构造函数，确保外部只能通过fromA生成合法实例，再借助fromJust（因实例合法性有保障，不会触发异常）实现f0：

{-# LANGUAGE RecordWildCards #-}
module ProperA (ProperA, fromA, f0) where

import Data.Maybe (fromJust)

-- 隐藏构造函数，仅导出类型本身
newtype ProperA a = ProperA { getA :: a }

-- 合法性判断逻辑，示例为字符串非空检查
isProper :: String -> Bool
isProper = not . null

-- 仅生成合法的ProperA实例
fromA :: String -> Maybe (ProperA String)
fromA x = if isProper x then Just (ProperA x) else Nothing

-- 原函数，示例为字符串拆分为首字符和剩余部分
f :: String -> Maybe (Char, String)
f = uncons

-- 安全的f0实现，无case表达式
f0 :: ProperA String -> (Char, String)
f0 = fromJust . f . getA

其他函数式语言的解决方案 #

Elm #

Elm无私有构造函数，但可通过模块隐藏构造函数实现封装，利用Maybe.withDefault（默认值永远不会触发）：

module ProperA exposing (ProperA, fromA, f0)

type ProperA = ProperA String

isProper : String -> Bool
isProper = not << String.isEmpty

fromA : String -> Maybe ProperA
fromA s = if isProper s then Just (ProperA s) else Nothing

f : String -> Maybe (Char, String)
f = String.uncons

-- 默认值仅为语法补全，因ProperA实例均合法，永远不会执行
f0 : ProperA -> (Char, String)
f0 (ProperA s) = Maybe.withDefault (' ', "") (f s)

Scala #

使用私有构造函数的类，伴生对象提供生成入口，直接调用Option.get（安全无异常）：

class ProperA private (val value: String)

object ProperA {
  def isProper(s: String): Boolean = s.nonEmpty
  def fromA(s: String): Option[ProperA] = if (isProper(s)) Some(new ProperA(s)) else None
}

def f(s: String): Option[(Char, String)] = if (s.nonEmpty) Some((s.head, s.tail)) else None

def f0(p: ProperA): (Char, String) = f(p.value).get

Idris（依赖类型方案） #

通过依赖类型将合法性证明嵌入类型，编译器直接排除不可能分支，无需额外处理：

data ProperA : Type -> Type where
  ProperA : (a : String) -> (prf : isProper a = True) -> ProperA String

isProper : String -> Bool
isProper = not . null

fromA : String -> Maybe (ProperA String)
fromA a = case isProper a of
  True => Just (ProperA a Refl)
  False => Nothing

f : String -> Maybe (Char, String)
f = strUncons

-- 编译器通过prf证明f a必为Just，无需处理Nothing分支
f0 : ProperA String -> (Char, String)
f0 (ProperA a prf) = let Just res = f a in res

核心思想 #

通过封装合法输入的包装类型，将运行时的合法性检查提前到编译阶段，从类型层面彻底排除非法输入的可能性，避免冗余的Maybe分支处理，实现类型安全的"不可能状态不可能"。

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