Bókarkaflar - HR
Varanleg URI fyrir þennan undirflokkhttps://hdl.handle.net/20.500.11815/1142
Skoða
Nýlegt
Verk Additive cellular automata graded-monadically(ACM, 2023-10-22) Capobianco, Silvio; Uustalu, Tarmo; Department of Computer Science (RU); Tölvunarfræðideild (HR); School of Technology (RU); Tæknisvið (HR)Cellular automata are an archetypical comonadic notion of computation in that computation happens in the coKleisli category of a comonad. In this paper, we show that they can also be viewed as graded comonadic—a perspective that turns out to be both more informative and also more basic. We also discuss additive cellular automata to show that they admit both a graded comonadic and a graded monadic view. That these two perspectives are simultaneously available in this special case arises from a graded version of an observation by Kleiner about adjoint comonad-monad pairs.Verk Degrading lists(ACM, 2020-09-08) McDermott, Dylan; Piróg, Maciej; Uustalu, Tarmo; Department of Computer Science; Tölvunarfræðideild (HR); School of Technology (RU); Tæknisvið (HR)We discuss the relationship between monads and their known generalisation, graded monads, which are especially useful for modelling computational effects equipped with a form of sequential composition. Specifically, we ask if a graded monad can be extended to a monad, and when such a degrading is in some sense canonical. Our particular examples are the graded monads of lists and non-empty lists indexed by their lengths, which gives us a pretext to study the space of all (non-graded) monad structures on the list and non-empty list endofunctors. We show that, in both cases, there exist infinitely many monad structures. However, while there are at least two ways to complete the graded monad structure on length-indexed lists to a monad structure on the list endofunctor, such a completion for non-empty lists is unique.Verk A type system with subtyping for WebAssembly’s stack polymorphism(Springer, 2022-10-03) McDermott, Dylan; Morita, Yasuaki; Uustalu, Tarmo; Department of Computer Science (RU); Tölvunarfræðideild (HR); School of Technology (RU); Tæknisvið (HR)We propose a new type system for WebAssembly. It is a refinement of the type system from the language specification and is based on type qualifiers and subtyping. In the WebAssembly specification, a typable instruction sequence gets many different types, depending in particular on whether it contains instructions such as br (unconditional branch) that are stack-polymorphic in an unusual way. But one cannot single out a canonical type for a typable instruction sequence satisfactorily. We introduce qualifiers on code types to distinguish between the two flavors of stack polymorphism that occur in WebAssembly and a subtyping relation on such qualified types. Our type system gives every typable instruction sequence a canonical type that is principal. We show that the new type system is in a precise relationship to the type system given in the WebAssembly specification. In addition, we describe a typed functional-style big-step semantics based on this new type system underpinned by an indexed graded monad and prove that it prevents stack-manipulation related runtime errors. We have formalized our type system, inference algorithm, and semantics in Agda.Verk Flexibly graded monads and graded algebras(Springer, 2022-09-22) McDermott, Dylan; Uustalu, Tarmo; Department of Computer Science (RU); Tölvunarfræðideild (HR); School of Technology (RU); Tæknisvið (HR)When modelling side-effects using a monad, we need to equip the monad with effectful operations. This can be done by noting that each algebra of the monad carries interpretations of the desired operations. We consider the analogous situation for graded monads, which are a generalization of monads that enable us to track quantitative information about side-effects. Grading makes a significant difference: while many graded monads of interest can be equipped with similar operations, the algebras often cannot. We explain where these operations come from for graded monads. To do this, we introduce the notion of flexibly graded monad, for which the situation is similar to the situation for ordinary monads. We then show that each flexibly graded monad induces a canonical graded monad in such a way that operations for the flexibly graded monad carry over to the graded monad. In doing this, we reformulate grading in terms of locally graded categories, showing in particular that graded monads are a particular kind of relative monad. We propose that locally graded categories are a useful setting for work on grading in general.Verk Algebraic and coalgebraic perspectives on interaction laws(Springer, 2020) Uustalu, Tarmo; Voorneveld, Niels; Department of Computer Science (RU); Tölvunarfræðideild (HR); School of Technology (RU); Tæknisvið (HR)Monad algebras, turning computations over return values into values, are used to handle algebraic effects invoked by programs, whereas comonad coalgebras, turning initial states into environments (“cocomputations”) over states, describe production of coalgebraic coeffects that can respond to effects. (Monad-comonad) interaction laws by Katsumata et al. describe interaction protocols between a computation and an environment. We show that any triple of those devices can be combined into a single algebra handling computations over state predicates. This method yields an isomorphism between the category of interaction laws, and the category of so-called merge functors which merge algebras and coalgebras to form combined algebras. In a similar vein, we can combine interaction laws with coalgebras only, retrieving Uustalu’s stateful runners. If instead we combine interaction laws with algebras only, we get a novel concept of continuation-based runners that lift an environment of value predicates to a single predicate on computations of values. We use these notions to study different running examples of interactions of computations and environments.Verk Project Creativity: Using Active Imagination for Project Innovation(University of Technology, Sydney, 2018-06-08) Jonasson, Haukur Ingi; Ingason, Helgi; Tækni- og verkfræðideild (HR); School of Science and Engineering (RU)Project management is essentially about solving problems and getting things done. The ability to imagine is a crucial ability when it comes to finding solutions and actualizing them. This paper looks at how creativity can, on an individual, team and organizational level, be fostered in project, program, and portfolio (PPP) management. The paper defines the human imagination as an essential component of higher order thinking—creative, critical and ethical thinking. It is essential to initiate new projects, deal with problems, enhance job satisfaction and give meaning to work life. The paper investigates a suggested use of Carl Jung´s ‘active imagination’ as a cognitive method to spark individual creativity and promote “a higher level of personal and collective self-actualization” in project work. It explores how to foster collective creativity in project teams, project management offices (PMOs), departments and organizations. The paper then argues for the centrality of creativity as a means to foster a more critical, ethical and sustainable approach to future challenges faced both in PPP management and for humankind in general.