Underlägsen typ

Den lägsta typen ( nolltyp , tom typ ) är ett objekt som används i vissa typteorier och programmeringsspråk som motsvarar en typ utan värden. Den matematiska standardnotationen är upper tack ( ). Inom ramen för Curry-Howard-korrespondensen motsvarar den lägsta typen en logisk falsk formel.

I subtypingsystem är den lägsta typen en subtyp av alla typer [1] ; men det omvända kanske inte är sant - i vissa fall är undertypen av alla typer inte nödvändigtvis den lägsta. Vissa typsystem introducerar ett dubbelt koncept - den högsta typen , som täcker alla möjliga värden i systemet.

I programmering används ofta den lägsta typen som returvärde för en funktion för att visa funktionsdivergens: när funktionen inte returnerar några resultat till den som ringer. Stöds i Haskell (sedan 2010), Common Lisp (symbol NIL), Scala ( Nothing; används även för kovarians av parametriserade typer ), Rust (experimentell datatyp, betecknad som !; finns i signaturen för funktioner som garanterat inte returnerar några värden, för till exempel när anrop panic!()eller oändlig loop, och som returtyp för kontrollflödesoperatorer som break[ return)2 ] , Ceylon ( Nothing)[3] , Julia ( Union{})[4] , TypeScript ( never) [5] [6] , JavaScript med Closure Compiler -kommentarer ( !Null), PHP ( never), Python ( typing.NoReturn) [7] , Kotlin ( Nothing)[8] , Elm ( Never) [9] , D ( noreturn) [10] .

Anteckningar

1. ↑ Piers Benjamin S. (1997). "Begränsad kvantifiering med en lägre gräns." CiteSeerX  10.1.1.17.9230 .
2. ↑ Den primitiva typen aldrig . Rust Standardbiblioteksdokumentation . Hämtad 24 september 2020. Arkiverad från originalet 23 september 2020. (obestämd)
3. ↑ Kapitel 3. Typsystem - 3.2.5. Underlägsen typ . Ceylon programmeringsspråk . Red Hat, Inc. Hämtad 19 februari 2017. Arkiverad från originalet 20 februari 2017. (obestämd)
4. ↑ Fundamentals of the Julia Programming Language , < https://docs.julialang.org/en/v1/base/base/ > Arkiverad 25 juli 2021 på Wayback Machine 
5. ↑ The never type, TypeScript 2.0 release notes , Microsoft, 2016-10-06 , < https://www.typescriptlang.org/docs/handbook/release-notes/typescript-2-0.html#the-never-type > . Hämtad 1 november 2019. Arkiverad 30 oktober 2019 på Wayback Machine 
6. ↑ The never type, TypeScript 2.0 release notes, källkod , Microsoft, 2016-10-06 , < https://github.com/microsoft/TypeScript-Handbook/blob/bb3564f4f06dd776d430198a137ae90590454/pagesnot9000/pages/2009 md#the-never-type > . Hämtad 1 november 2019. Arkiverad 16 juli 2021 på Wayback Machine 
7. ↑ typing.NoReturn, typing — Typ Tips Support, Python Language Documentation, Python Software Foundation , < https://docs.python.org/3/library/typing.html#typing.NoReturn > . Hämtad 25 februari 2020. Arkiverad 21 februari 2020 på Wayback Machine 
8. ↑ Ingenting , < https://kotlinlang.org/api/latest/jvm/stdlib/kotlin/-nothing.html > . Hämtad 15 maj 2020. Arkiverad 25 februari 2020 på Wayback Machine 
9. ↑ Aldrig , < https://package.elm-lang.org/packages/elm/core/latest/Basics#Never > . Hämtad 25 mars 2021. Arkiverad 10 april 2021 på Wayback Machine 
10. ↑ Typer - D programmeringsspråk . dlang.org . Hämtad: 31 juli 2022. (obestämd)

Länkar

• Pierce B. Skriver i programmeringsspråk. - Dobrosvet , 2012. - 680 sid. — ISBN 978-5-7913-0082-9 .