scholarly journals Decidable Subtyping for Path Dependent Types

2021 ◽  
Author(s):  
◽  
Julian Mackay
Keyword(s):  
Programming Language ◽  
Central Component ◽  
Dependent Types ◽  
Presenting Problems ◽  
Type Safety ◽  
Parametric Polymorphism ◽  
Programming Patterns ◽  
The Common ◽  
Path Dependent ◽  
Formal Properties

<p>Path dependent types form a central component of the Scala programming language. Coupled with other expressive type forms, path dependent types provide for a diverse set of concepts and patterns, from nominality to F-bounded polymorphism. Recent years have seen much work aimed at formalising the foundations of path dependent types, most notably a hard won proof of type safety. Unfortunately subtyping remains undecidable, presenting problems for programmers who rely on the results of their tools. One such tool is Dotty, the basis for the upcoming Scala 3. Another is Wyvern, a new programming language that leverages path dependent types to support both first class modules and parametric polymorphism. In this thesis I investigate the issues with deciding subtyping in Wyvern. I define three decidable variants that retain several key instances of expressiveness including the ability to encode nominality and parametric polymorphism. Wyvfix fixes types to the contexts they are defined in, thereby eliminating expansive environments. Wyvnon-μ removes recursive subtyping, thus removing the key source of expansive environments during subtyping. Wyvμ places a syntactic restriction on the usage of recursive types. I discuss the formal properties of these variants, and the implications each has for expressing the common programming patterns of path dependent types. I have also mechanized the proofs of decidability for both Wyvfix and Wyvμ in Coq.</p>

scholarly journals Decidable Subtyping for Path Dependent Types

2021 ◽  
Author(s):  
◽  
Julian Mackay
Keyword(s):  
Programming Language ◽  
Central Component ◽  
Dependent Types ◽  
Presenting Problems ◽  
Type Safety ◽  
Parametric Polymorphism ◽  
Programming Patterns ◽  
The Common ◽  
Path Dependent ◽  
Formal Properties

<p>Path dependent types form a central component of the Scala programming language. Coupled with other expressive type forms, path dependent types provide for a diverse set of concepts and patterns, from nominality to F-bounded polymorphism. Recent years have seen much work aimed at formalising the foundations of path dependent types, most notably a hard won proof of type safety. Unfortunately subtyping remains undecidable, presenting problems for programmers who rely on the results of their tools. One such tool is Dotty, the basis for the upcoming Scala 3. Another is Wyvern, a new programming language that leverages path dependent types to support both first class modules and parametric polymorphism. In this thesis I investigate the issues with deciding subtyping in Wyvern. I define three decidable variants that retain several key instances of expressiveness including the ability to encode nominality and parametric polymorphism. Wyvfix fixes types to the contexts they are defined in, thereby eliminating expansive environments. Wyvnon-μ removes recursive subtyping, thus removing the key source of expansive environments during subtyping. Wyvμ places a syntactic restriction on the usage of recursive types. I discuss the formal properties of these variants, and the implications each has for expressing the common programming patterns of path dependent types. I have also mechanized the proofs of decidability for both Wyvfix and Wyvμ in Coq.</p>

Foundations of path-dependent types

2014 ◽  
Vol 49 (10) ◽  
pp. 233-249 ◽  
Author(s):  
Nada Amin ◽  
Tiark Rompf ◽  
Martin Odersky
Keyword(s):  
Dependent Types ◽  
Path Dependent

Wittenberg Reformers

2021 ◽  
pp. 27-51
Author(s):  
Esther Chung-Kim
Keyword(s):  
Catholic Church ◽  
Central Component ◽  
Poor Relief ◽  
System P ◽  
Theological Foundations ◽  
The Common ◽  
Per Se ◽  
Relief System ◽  
Mendicant Orders ◽  
The Church

Wittenberg reformers supported the transfer of formerly Catholic Church properties to government possession. This secularization of church property did not mean a rejection of religion per se; on the contrary, secularization of church property meant that political rulers consolidated the scattered ecclesiastical properties and possessions into a common chest so that they could support the reform of the church. While Martin Luther and Andreas Karlstadt denounced mendicant orders for their begging lifestyle, they called for cities to care for their resident poor so that begging would be obsolete. Their critique became the catalyst for change, including an educated pastorate with preaching as a central component of worship, schools for boys and girls, and a system of poor relief funded by monastic foundations, confraternities, and donations. In the transfer of property to the common chest, Wittenberg reformers were crucial in providing the theological foundations for the transition to a centralized poor relief system.

scholarly journals Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala

2020 ◽  
Vol 30 ◽  
Author(s):  
JONATHAN IMMANUEL BRACHTHÄUSER ◽  
PHILIPP SCHUSTER ◽  
KLAUS OSTERMANN
Keyword(s):  
Type System ◽  
Dependent Types ◽  
Individual Effect ◽  
Library Design ◽  
Programming Paradigm ◽  
Intersection Types ◽  
Delimited Continuations ◽  
Path Dependent

Abstract Effect handlers are a promising way to structure effectful programs in a modular way. We present the Scala library Effekt, which is centered around capability passing and implemented in terms of a monad for multi-prompt delimited continuations. Effekt is the first library implementation of effect handlers that supports effect safety and effect polymorphism without resorting to type-level programming. We describe a novel way of achieving effect safety using intersection types and path-dependent types. The effect system of our library design fits well into the programming paradigm of capability passing and is inspired by the effect system of Zhang & Myers (2019, Proc. ACM Program. Lang.3(POPL), 5:1-5:29). Capabilities carry an abstract type member, which represents an individual effect type and reflects the use of the capability on the type level. We represent effect rows as the contravariant intersection of effect types. Handlers introduce capabilities and remove components of the intersection type. Reusing the existing type system of Scala, we get effect subtyping and effect polymorphism for free.

scholarly journals A Rice Gene for Microbial Symbiosis,Oryza sativaCCaMK, Reduces CH4Flux in a Paddy Field with Low Nitrogen Input

2014 ◽  
Vol 80 (6) ◽  
pp. 1995-2003 ◽  
Author(s):  
Zhihua Bao ◽  
Aya Watanabe ◽  
Kazuhiro Sasaki ◽  
Takashi Okubo ◽  
Takeshi Tokida ◽  
...  
Keyword(s):  
Copy Number ◽  
Root Zone ◽  
Central Component ◽  
Symbiotic Relationships ◽  
Dependent Protein ◽  
The Common ◽  
Microbial Symbiosis ◽  
Methyl Coenzyme M Reductase ◽  
Low Nitrogen

ABSTRACTPlants have mutualistic symbiotic relationships with rhizobia and fungi by the common symbiosis pathway, of which Ca2+/calmodulin-dependent protein kinase (encoded byCCaMK) is a central component. AlthoughOryza sativaCCaMK(OsCCaMK) is required for fungal accommodation in rice roots, little is known about the role ofOsCCaMKin rice symbiosis with bacteria. Here, we report the effect of aTos17-inducedOsCCaMKmutant (NE1115) on CH4flux in low-nitrogen (LN) and standard-nitrogen (SN) paddy fields compared with wild-type (WT) Nipponbare. The growth of NE1115 was significantly decreased compared with that of the WT, especially in the LN field. The CH4flux of NE1115 in the LN field was significantly greater (156 to 407% in 2011 and 170 to 816% in 2012) than that of the WT, although no difference was observed in the SN field. The copy number ofpmoA(encodes methane monooxygenase in methanotrophs) was significantly higher in the roots and rhizosphere soil of the WT than in those of NE1115. However, themcrA(encodes methyl coenzyme M reductase in methanogens) copy number did not differ between the WT and NE1115. These results were supported by a13C-labeled CH4-feeding experiment. In addition, the natural abundance of15N in WT shoots (3.05‰) was significantly lower than in NE1115 shoots (3.45‰), suggesting greater N2fixation in the WT because of dilution with atmospheric N2(0.00‰). Thus, CH4oxidation and N2fixation were simultaneously activated in the root zone of WT rice in the LN field and both processes are likely controlled byOsCCaMK.

Integrated Services in Activation Policies in Finland and Italy: A Critical Appraisal

2008 ◽  
Vol 7 (3) ◽  
pp. 379-392 ◽  
Author(s):  
Angela Genova
Keyword(s):  
Critical Appraisal ◽  
Integrated Services ◽  
Comparative Perspective ◽  
Welfare Regimes ◽  
Welfare Policies ◽  
Eu Member States ◽  
The Common ◽  
Path Dependent ◽  
Modes Of Governance

The integration of welfare services in activation policies has been one of the common answers to welfare challenges in EU member states over the last two decades. The process has been interwoven with the rescaling both downwards and upwards of welfare regulative authorities. The article discusses the role of integrated services in activation policies in relation to the centralisation and decentralisation of welfare policies in a comparative perspective of different EU welfare regimes and highlights the role of local institutional milieus in shaping path-dependent modes of governance in integrated services.

scholarly journals Parametric polymorphism and operational equivalence

2000 ◽  
Vol 10 (3) ◽  
pp. 321-359 ◽  
Author(s):  
ANDREW M. PITTS
Keyword(s):  
Programming Language ◽  
Functional Programming ◽  
Closure Operator ◽  
Lambda Calculus ◽  
Logical Relation ◽  
Data Types ◽  
Mathematical Properties ◽  
Parametric Polymorphism ◽  
Operational Behaviour

Studies of the mathematical properties of impredicative polymorphic types have for the most part focused on the polymorphic lambda calculus of Girard–Reynolds, which is a calculus of total polymorphic functions. This paper considers polymorphic types from a functional programming perspective, where the partialness arising from the presence of fixpoint recursion complicates the nature of potentially infinite (‘lazy’) data types. An approach to Reynolds' notion of relational parametricity is developed that works directly on the syntax of a programming language, using a novel closure operator to relate operational behaviour to parametricity properties of types. Working with an extension of Plotkin's PCF with ∀-types, lazy lists and existential types, we show by example how the resulting logical relation can be used to prove properties of polymorphic types up to operational equivalence.

scholarly journals Localized Lama Gradual Typing

2021 ◽  
Vol 33 (3) ◽  
pp. 61-76
Author(s):  
Viktor Sergeevich Kryshtapovich
Keyword(s):  
Programming Language ◽  
Type System ◽  
Scientific Research ◽  
Type Systems ◽  
Modern Approach ◽  
Type Safety ◽  
Current Implementation ◽  
Gradual Typing ◽  
Dynamic Typing ◽  
Static Typing

Gradual typing is a modern approach for combining benefits of static typing and dynamic typing. Although scientific research aim for soundness of type systems, many of languages intentionally make their type system unsound for speeding up performance. This paper describes an implementation of a dialect for Lama programming language that supports gradual typing with explicit annotation of dangerous parts of code. The target of current implementation is to grant type safety to programs while keeping their power of untyped expressiveness. This paper covers implementation issues and properties of created type system. Finally, some perspectives on improving precision and soundness of type system are discussed.

scholarly journals Plastics everywhere: first evidence of polystyrene fragments inside the common Antarctic collembolan Cryptopygus antarcticus

2020 ◽  
Vol 16 (6) ◽  
pp. 20200093 ◽  
Author(s):  
Elisa Bergami ◽  
Emilia Rota ◽  
Tancredi Caruso ◽  
Giovanni Birarda ◽  
Lisa Vaccari ◽  
...  
Keyword(s):  
Food Webs ◽  
Terrestrial Ecosystems ◽  
Enzymatic Digestion ◽  
Future Research ◽  
Central Component ◽  
Fildes Peninsula ◽  
Large Piece ◽  
The Common ◽  
Composition Structure ◽  
Potential Stressor

There is evidence and serious concern that microplastics have reached the most remote regions of the planet, but how far have they travelled in terrestrial ecosystems? This study presents the first field-based evidence of plastic ingestion by a common and central component of Antarctic terrestrial food webs, the collembolan Cryptopygus antarcticus . A large piece of polystyrene (PS) foam (34 × 31 × 5 cm) covered by microalgae, moss, lichens and microfauna was found in a fellfield along the shores of the Fildes Peninsula (King George Island). The application of an improved enzymatic digestion coupled with Fourier transform infrared microscopy (µ-FTIR), unequivocally detected traces of PS (less than 100 µm) in the gut of the collembolans associated with the PS foam and documented their ability to ingest plastic. Plastics are thus entering the short Antarctic terrestrial food webs and represent a new potential stressor to polar ecosystems already facing climate change and increasing human activities. Future research should explore the effects of plastics on the composition, structure and functions of polar terrestrial biota.

Sign in / Sign up

Export Citation Format

Share Document