Chciałem rozwiązać ten sam problem. Poniższa dyskusja na pewno bardzo mi pomogło:
Abusing the algebra of algebraic data types - why does this work?
Początkowo, ja też był zaniepokojony typów, takich jak forall a. a -> a. Potem miałem objawienie. Zdałem sobie sprawę, że typ forall a. a -> a był Mogensen-Scott encoding z unit type. Stąd miał tylko jednego mieszkańca. Podobnie, forall a. a jest kodowaniem Mogensen-Scott z bottom type. Stąd ma zero mieszkańców. Rozważmy następujące typy danych algebraicznych:
data Bottom -- forall a. a
data Unit = Unit -- forall a. a -> a
data Bool = False | True -- forall a. a -> a -> a
data Nat = Succ Nat | Zero -- forall a. (a -> a) -> a -> a
data List a = Cons a (List a) | Nil -- forall a b. (a -> b -> b) -> b -> b
algebraiczne typ danych jest sum z products. Będę używał składni ⟦τ⟧ do oznaczenia liczby mieszkańców typu τ.Istnieją dwa rodzaje typów Użyję w tym artykule: typy danych F
System, oblicza się według następującego BNF:
τ = α
| τ -> τ
| ∀ α. τ
algebraiczne typy danych, oblicza się według następującego BNF:
τ =
| α
| τ + τ
| τ * τ
| μ α. τ
Obliczanie liczby mieszkańców algebraicznych typu danych jest dość prosta:
⟦⟧ =
⟦τ¹ + τ²⟧ = ⟦τ¹⟧ + ⟦τ²⟧
⟦τ¹ * τ²⟧ = ⟦τ¹⟧ * ⟦τ²⟧
⟦μ α. τ⟧ = ⟦τ [μ α. τ/α]⟧
Rozważmy na przykład listy Typ danych μ β. α * β + 1:
⟦μ β. α * β + 1⟧ = ⟦(α * β + 1) [μ β. α * β + 1/β]⟧
= ⟦α * (μ β. α * β + 1) + 1⟧
= ⟦α * (μ β. α * β + 1)⟧ + ⟦1⟧
= ⟦α⟧ * ⟦μ β. α * β + 1⟧ + ⟦1⟧
= ⟦α⟧ * ⟦μ β. α * β + 1⟧ + 1
Jednak obliczenia liczby mieszkańców typ danych systemu F nie jest tak prosta. Niemniej jednak można to zrobić. Aby to zrobić, musimy przekonwertować typ danych System F na równoważny algebraiczny typ danych. Na przykład typ danych System F ∀ α. ∀ β. (α -> β -> β) -> β -> β jest odpowiednikiem typu danych listy algebraicznej: μ β. α * β + 1.
Pierwszą rzeczą, aby zauważyć, że chociaż rodzaj systemu F ∀ α. ∀ β. (α -> β -> β) -> β -> β posiada dwie uniwersalne kwantyfikatory jeszcze algebraiczną lista typ danych μ β. α * β + 1 ma tylko jeden (stały punkt) kwantyfikator (czyli algebraiczne typ danych jest lista jednokształtny).
Mimo że możemy utworzyć typ danych listy algebraicznej polimorficznej (tj. ∀ α. μ β. α * β + 1) i dodać regułę ⟦∀ α. τ⟧ = ∀ α. ⟦τ⟧, ale nie robimy tego, ponieważ niepotrzebnie komplikuje sprawy. Zakładamy, że typ polimorficzny został wyspecjalizowany do pewnego typu monomorficznego.
Pierwszym krokiem jest więc usunięcie wszystkich uniwersalnych kwantyfikatorów z wyjątkiem tego, które reprezentuje kwantyfikator "ustalonego punktu". Na przykład typ ∀ α. ∀ β. α -> β -> α staje się ∀ α. α -> β -> α.
Większość konwersji jest prosta ze względu na kodowanie Mogensen-Scotta. Na przykład:
∀ α. α = μ α. 0 -- bottom type
∀ α. α -> α = μ α. 1 + 0 -- unit type
∀ α. α -> α -> α = μ α. 1 + 1 + 0 -- boolean type
∀ α. (α -> α) -> α -> α = μ α. (α * 1) + 1 + 0 -- natural number type
∀ β. (α -> β -> β) -> β -> β = μ β. (α * β * 1) + 1 + 0 -- list type
Niektóre konwersje nie są jednak tak proste. Na przykład ∀ α. α -> β -> α nie reprezentuje prawidłowego typu danych zakodowanych przez Mogensen-Scott. Mimo to, możemy uzyskać prawidłową odpowiedź poprzez żonglowanie typami trochę:
⟦∀ α. α -> β -> α⟧ = ⟦β -> ∀ α. α -> α⟧
= ⟦∀ α. α -> α⟧^⟦β⟧
= ⟦μ α. 1 + 0⟧^⟦β⟧
= ⟦μ α. 1⟧^⟦β⟧
= ⟦1⟧^⟦β⟧
= 1^⟦β⟧
= 1
dla innych typów musimy użyć kilku sztuczek:
∀ α. (α, α) -> (α, α) = (∀ α. (α, α) -> α, ∀ α. (α, α) -> α)
= (∀ α. α -> α -> α, ∀ α. α -> α -> α)
⟦∀ α. α -> α -> α⟧ = ⟦μ α. 1 + 1 + 0⟧
= ⟦μ α. 2⟧
= ⟦2⟧
= 2
⟦∀ α. (α, α) -> (α, α)⟧ = ⟦∀ α. α -> α -> α⟧ * ⟦∀ α. α -> α -> α⟧
= 2 * 2
= 4
Chociaż istnieje prosty algorytm, który da nam numer mieszkańców typu kodowanego przez Mogensen-Scott, ale nie mogę wymyślić żadnego ogólnego algorytmu, który da nam liczbę mieszkańców dowolnego typu polimorficznego.
W rzeczywistości mam bardzo silne przeczucie, że obliczanie liczby mieszkańców dowolnego rodzaju polimorficznego jest problemem nierozstrzygalnym. Dlatego uważam, że nie ma algorytmu, który da nam liczbę mieszkańców dowolnego rodzaju polimorficznego w ogóle.
Niemniej jednak uważam, że używanie typów kodowanych przez Mogensen-Scott to świetny początek. Mam nadzieję że to pomoże.