这是不可能的，如果不使用undefined作为另一个评论者提到。让我们用反例来证明这一点。假设有这样一个函数：

f :: a -> a

当你说它和id不一样时，这意味着你不能定义：

f x = x

然而，考虑a是()类型的情况：

f () = ...

f唯一可能返回的结果是()，但这与id的实现相同，因此是矛盾的。
更复杂和严格的答案是证明类型a -> a必须同构于()。当我们说两个类型a和b是同构的，这意味着我们可以定义两个函数：

fw :: a -> b
bw :: b -> a

.这样：

fw . bw = id
bw . fw = id

当第一个类型是a -> a，第二个类型是()时，我们可以很容易地做到这一点：

fw :: (forall a . a -> a) -> ()
fw f = f ()

bw :: () -> (forall a . a -> a)
bw () x = x

然后我们可以证明：

fw . bw
= \() -> fw (bw ())
= \() -> fw (\x -> x)
= \() -> (\x -> x) ()
= \() -> ()
= id

bw . fw
= \f -> bw (fw f)
-- For this to type-check, the type of (fw f) must be ()
-- Therefore, f must be `id`
= \f -> id
= \f -> f
= id

当你证明两个类型是同构的，你知道的一件事是，如果一个类型是由有限数量的元素，所以必须另一个。由于()类型只包含一个值：

data () = ()

这意味着类型(forall a . a -> a)也必须被恰好一个值占据，这恰好是id的实现。
编辑：有些人评论说同构的证明不够严格，所以我将引用米田引理，当翻译成Haskell时，它说对于任何函子f：

(forall b . (a -> b) -> f b) ~ f a

其中~表示(forall b . (a -> b) -> f b)同构于f a。如果你选择Identity函子，这可以简化为：

(forall b . (a -> b) -> b) ~ a

.如果选择a = ()，则进一步简化为：

(forall b . (() -> b) -> b) ~ ()

你可以很容易地证明() -> b同构于b：

fw :: (() -> b) -> b
fw f = f ()

bw :: b -> (() -> b)
bw b = \() -> b

fw . bw
= \b -> fw (bw b)
= \b -> fw (\() -> b)
= \b -> (\() -> b) ()
= \b -> b
= id

bw . fw
= \f -> bw (fw f)
= \f -> bw (f ())
= \f -> \() -> f ()
= \f -> f
= id

因此，我们可以使用它来最终专门化Yoneda同构：

(forall b . b -> b) ~ ()

也就是说任何forall b . b -> b类型的函数都同构于()。米田引理提供了我的证明所缺少的严密性。

让我来阐述一下dbaupp的评论。任何a -> a类型的函数也会给予() -> ()类型的函数，所以我将先看这个子问题。
Haskell类型和函数的通常语义是将类型表示为点链完全偏序，将函数表示为连续函数。类型()由两个元素的集合 {x1，（）} 表示，顺序为 * x2，（）*。在普通集合论中，有2^2=4个函数从这个集合到它本身，但只有三个是连续的：

• f1：，（），
• f2：，（）（），和
• f3：（），（）（）.

因此，在我们的语义模型中，有三个不同的() -> ()类型函数。但是哪一个可以在Haskell中实现呢？所有人！

• f1 _ = undefined（或f1 x = f1 x）
• f2 x = x（或f2 = id）
• f3 _ = ()（或f3 = const ()）

查看这些定义，您可以看到f1和f2也可以用于定义a -> a类型的函数。因为它们在()上已经做了不同的事情，所以它们是不同的。所以我们至少有两个不同的a -> a类型的函数。
在上面的语义模型中，有更多的a -> a类型的函数，但这些函数在Haskell中是不可表达的（这与参数性和Wadler的Theorems for Free有关）。要正确证明f1和f2是唯一的这类函数似乎并不容易，因为这取决于Haskell语言不允许什么（例如：在参数的类型上没有模式匹配）。

除非你愿意使用undefined或bottom（一个非终止表达式），否则实际上没有其他函数满足该类型。
这是Haskell类型系统的一大优势。可以将可以通过编译器的可能函数严格限制为明显正确的函数。一个极端的例子，参见djinn--它接受一个类型，并生成与该类型匹配的可能函数。即使对于真实的、复杂的例子，这个列表也往往很短。

这里的关键是要明白，我们对a一无所知，尤其是我们没有办法生成一个新的a，或者将它转换为不同的东西。因此，我们没有选择返回它（或底部值）。一旦我们有关于a的更多信息（例如，a context绑定），我们可以用它做更有趣的事情：

f :: Monoid a => a -> a
f _ = mempty

或

f :: Monoid a => a -> a
f x = x `mappend` x `mappend` x

或者，如果你有像f :: (a, a) -> a这样的选择，你有两种可能的实现（再次忽略底部值），但是对于f :: (a, b) -> a，你又回到了一种实现，这与fst相同：虽然用一对相同的类型调用f是有效的，例如。f ("x", "y")，可以确定f的行为与fst类似，因为在f的实现中，您无法测试两种参数类型是否相同。同样，f :: (a -> b) -> a -> b也只有一个非底层版本。
多态性限制了自由度，因为你对你的参数一无所知，在某些情况下，它归结为一个非底部版本。

正如其他人提到的，不可能存在这样的其他 total 函数。（如果我们不局限于全函数，那么我们可以通过undefined来容纳任何类型。
我将尝试给予一个基于λ演算的理论解释：
为了简单起见，让我们将自己限制在λ项（我们可以将任何Haskell表达式转换为λ项）。对于λ项M，如果M ≡ A N1 ... Nk和A不是应用程序（k也可以为零），我们称A为它的 head。注意，如果M是正规形式，那么A不能是λ-抽象，除非k = 0。
设M :: a -> a是正规形式的λ项。由于上下文中没有变量，因此M不能是变量，也不能是应用程序。如果是的话，它的头应该是一个变量。所以M必须是λ-抽象，它必须是M ≡ λ(x:a).N。
现在N必须是a类型，正式的{x:a}⊢N:a。如果N是一个λ-抽象，它的类型将是σ -> τ，这是不可能的。如果N是一个函数应用程序，那么它的head必须是一个变量，而上下文中唯一的变量是x。但是由于x:a，我们不能将x应用于任何东西，x P不能用于任何P。所以唯一的可能性是N ≡ x。因此，M必须是λ(x:a).x。
（如果可能的话，请纠正我的英语。特别是，我不知道如何使用subjunctive的权利）。

这里有一个：

Prelude> t = \x -> (\y -> y) x
Prelude> :t t
t :: p -> p
Prelude> t 3
3
Prelude> t "hello"
"hello"