Jaki jest typ dolny?

Question

W wikipedia, bottom type jest po prostu zdefiniowany jako "typ, który nie ma wartości". Jeśli jednak ten typ pusty jest b, produkt typu (b,b) również nie ma wartości, ale wydaje się inny niż b. Zgadzam się, że dno jest niezamieszkałe, ale nie sądzę, że ta właściwość wystarczy, by to zdefiniować.

W przypadku Curry-Howard correspondence spód jest powiązany z fałszem matematycznym. Teraz istnieje logiczna zasada stwierdzająca, że ​​od Fałszy wynika każda propozycja. Według Curry-Howarda, oznacza to, że typ forall a. bottom -> a jest zamieszkany, tj. Istnieje rodzina funkcji f :: forall a. bottom -> a.

Jakie są te funkcje f? Czy pomagają zdefiniować dno, może jako nieskończony produkt wszystkich typów forall a. a?

Answer 1

w matematyce

Dno jest typ, który nie ma żadnej wartości. Oznacza to, że każdy pusty typ może odgrywać rolę dolną.

Te funkcje f :: forall a . Bottom -> a są puste. "puste" w ustawionej teoretycznej definicji funkcji.

w programowaniu

Poświęcając konkretny typ pusty mieć go jako dołu przez bibliotekę bazowego języka programowania jest dla wygody. Czytelność i kompatybilność kodu przynosi korzyści wszystkim, którzy używają tego samego pustego typu co dno.

W Haskell

Pozwól nam odnosić się do nich z bardziej przyjaznych nazw "Dół" -> "pustkę", "f" -> "absurdalne".

{-# LANGUAGE EmptyDataDecls #-} 
data Void 

Ta definicja nie zawiera żadnych konstruktorów => nie można utworzyć instancji => jest pusta.

absurd :: Bottom -> a 
absurd = \ case {} 

W wyrażeniu przypadku nie musimy zajmować się żadnymi przypadkami, ponieważ ich nie ma.

Są już defined in package base