在Haskell里，每個類型都可以構造出來一個此類型的表達式嗎？

01-27

比如是否存在一個類型t使得t是一個合法的haskell類型但是卻沒有符合語法的表達式使得s的類型是t。我剛想到的一個例子是(a -&> Bool) -&> a，我嘗試了好久，似乎確實構造不出一個let f = ....., 使得f的類型是這個。請問這個有嚴格的證明嗎？如果確實存在這樣的類型，那麼判斷這種類型的充分必要條件是什麼？

一個類型「是否有值」這個屬性，稱為inhabited

首先，所有kind為*的Haskell type（也就是排除了unlifted的那些），都是inhabited by bottom的，也就是說，undefined，或者let x = x in x都可以是這些類型的值

然後，除去bottom這部分，給定type signature判定是否有inhabitant，這個理論基礎是Philip Wadler的free theorems，可以從https://gist.github.com/pchiusano/444de1f222f1ceb09596看起，具體到你這個例子，回答是不能。因為一個含有多態類型的函數，要產生多態輸出的唯一來源是其參數，而你的參數只有(a -&> Bool)沒有a，所以不能輸出a

type inhabitation問題是不可判定的，但是對於你的例子，可以證明不能。

因為(a -&> Bool) -&> a 裡面沒有值。

證明如下：

{-# LANGUAGE RankNTypes #-}

type FALSE = forall b. b

proof :: (forall a. (a -&> Bool) -&> a) -&> FALSE

proof f = f (x -&> True)

註：

1. FALSE定義成forall b. b，因為forall b. b可以推出一切。你也可以用其它的FALSE定義，比如forall b. (b -&> b) -&> b，或者更複雜的。

2. (a -&> Bool) -&> a是forall a. (a -&> Bool) -&> a的縮寫。

3. 對於任何一個類型t，如果你能寫出t -&> FALSE的（非死循環，不拋出異常，不調用unsafeXX）的Haskell函數，那麼等效於你構造出了t -&> False的證明項，也就是說你證明了t -&> False，即t為假，即類型t中無值。

這個是type inhabitation問題

對於simple typed $lambda$ calculus，是可判定的，且為PSPACE-complete

System $F$ 和System $F_omega$ 不可判定，不太了解Haskell不可判定的原因（大概和多態有關。。）

一個思路是轉化為對應或者相關的邏輯系統（不一定都能找到），比如simple typed $lambda$ calculus和直覺主義命題邏輯，然用邏輯學方法如finite model property，cut-elimination等來證明判定性問題，reduce到SAT、QBF、 $exists MSO$ 或者xx自動機之類的以確定複雜度。。

可以，haskell 里有個表達式叫 undefined，可以具有任意類型