Ringere type

Den laveste type ( nul type , tom type ) er et objekt, der bruges i nogle typeteorier og programmeringssprog, der svarer til en type uden værdier. Den matematiske standardnotation er upper tack ( ). Inden for rammerne af Curry-Howard-korrespondancen svarer den laveste type til en logisk falsk formel.

I undertypesystemer er den laveste type en undertype af alle typer [1] ; det modsatte er dog muligvis ikke sandt - i nogle tilfælde vil undertypen af ​​alle typer ikke nødvendigvis være den laveste. Nogle typesystemer introducerer et dobbelt koncept - den højeste type , der dækker alle mulige værdier i systemet.

I programmering bruges den laveste type som returværdi af en funktion ofte til at vise funktionsdivergens: når funktionen ikke returnerer nogen resultater til den, der ringer. Understøttet i Haskell (siden 2010), Common Lisp (symbol NIL), Scala ( Nothing; bruges også til kovarians af parametriserede typer ), Rust (eksperimentel datatype, betegnet som !; til stede i signaturen af ​​funktioner, der garanteret ikke returnerer nogen værdier, for f.eks. når opkald panic!()eller uendelig sløjfe, og som returtype for kontrolflowoperatorer såsom break[ return)2] , Ceylon ( Nothing)[3] , Julia ( Union{})[4] , TypeScript ( never) [5] [6] , JavaScript med Closure Compiler- annoteringer ( !Null), PHP ( never), Python ( typing.NoReturn) [7] , Kotlin ( Nothing)[8] , Elm ( Never) [9] , D ( noreturn) [10] .

Noter

1. ↑ Piers Benjamin S. (1997). "Begrænset kvantificering med en nedre grænse." CiteSeerX  10.1.1.17.9230 .
2. ↑ Den primitive type aldrig . Rust Standard biblioteksdokumentation . Hentet 24. september 2020. Arkiveret fra originalen 23. september 2020. (ubestemt)
3. ↑ Kapitel 3. Typesystem - 3.2.5. ringere type . Ceylon-programmeringssproget . Red Hat, Inc. Hentet 19. februar 2017. Arkiveret fra originalen 20. februar 2017. (ubestemt)
4. ↑ Fundamentals of the Julia Programming Language , < https://docs.julialang.org/en/v1/base/base/ > Arkiveret 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 > . Hentet 1. november 2019. Arkiveret 30. oktober 2019 på Wayback Machine 
6. ↑ The never type, TypeScript 2.0 release notes, kildekode , Microsoft, 2016-10-06 , < https://github.com/microsoft/TypeScript-Handbook/blob/bb3564f4f06dd776d430198a137ae90580445%209dlease md#the-never-type > . Hentet 1. november 2019. Arkiveret 16. juli 2021 på Wayback Machine 
7. ↑ typing.NoReturn, typing — Type Tip Support, Python Language Documentation, Python Software Foundation , < https://docs.python.org/3/library/typing.html#typing.NoReturn > . Hentet 25. februar 2020. Arkiveret 21. februar 2020 på Wayback Machine 
8. ↑ Intet , < https://kotlinlang.org/api/latest/jvm/stdlib/kotlin/-nothing.html > . Hentet 15. maj 2020. Arkiveret 25. februar 2020 på Wayback Machine 
9. ↑ Aldrig , < https://package.elm-lang.org/packages/elm/core/latest/Basics#Never > . Hentet 25. marts 2021. Arkiveret 10. april 2021 på Wayback Machine 
10. ↑ Typer - D programmeringssprog . dlang.org . Hentet: 31. juli 2022. (ubestemt)

Links

• Pierce B. Skriver i programmeringssprog. - Dobrosvet , 2012. - 680 s. — ISBN 978-5-7913-0082-9 .