-
Extensible Recursive Functions, Algebraically
Authors:
Alex Hubers,
Apoorv Ingle,
Andrew Marmaduke,
J. Garrett Morris
Abstract:
We explore recursive programming with extensible data types. Row types make the structure of data types first class, and can express a variety of type system features from subtyping to modular combination of case branches. Our goal is the modular combination of recursive types and of recursive functions over them. The most significant challenge is in recursive function calls, which may need to acc…
▽ More
We explore recursive programming with extensible data types. Row types make the structure of data types first class, and can express a variety of type system features from subtyping to modular combination of case branches. Our goal is the modular combination of recursive types and of recursive functions over them. The most significant challenge is in recursive function calls, which may need to account for new cases in a combined type. We introduce bounded algebras, Mendler-style descriptions of recursive functions in which recursive calls can happen at larger types, and show that they provide expressive recursion over extensible data types. We formalize our approach in R$ωμ$, a small extension of an existing row type theory with support for recursive terms and types, and mechanize the metatheory of R$ωμ$ via an embedding in Agda
△ Less
Submitted 15 October, 2024;
originally announced October 2024.
-
Generic Programming with Extensible Data Types; Or, Making Ad Hoc Extensible Data Types Less Ad Hoc
Authors:
Alex Hubers,
J. Garrett Morris
Abstract:
We present a novel approach to generic programming over extensible data types. Row types capture the structure of records and variants, and can be used to express record and variant subtyping, record extension, and modular composition of case branches. We extend row typing to capture generic programming over rows themselves, capturing patterns including lifting operations to records and variations…
▽ More
We present a novel approach to generic programming over extensible data types. Row types capture the structure of records and variants, and can be used to express record and variant subtyping, record extension, and modular composition of case branches. We extend row typing to capture generic programming over rows themselves, capturing patterns including lifting operations to records and variations from their component types, and the duality between cases blocks over variants and records of labeled functions, without placing specific requirements on the fields or constructors present in the records and variants. We formalize our approach in System Rω, an extension of Fω with row types, and give a denotational semantics for (stratified) Rω in Agda.
△ Less
Submitted 19 July, 2023; v1 submitted 17 July, 2023;
originally announced July 2023.
-
Sketched Floor plans versus SLAM maps: A Comparison
Authors:
Leo Bowen-Biggs,
Suzanne Dazo,
Yili Zhang,
Alex Hubers,
Matthew Rueben,
Ross Sowell,
William D. Smart,
Cindy Grimm
Abstract:
Maps --- specifically floor plans --- are useful for a variety of tasks from arranging furniture to designating conceptual or functional spaces (e.g., kitchen, walkway). We present a simple algorithm for quickly laying a floor plan (or other conceptual map) onto a SLAM map, creating a one-to-one mapping between them. Our goal was to enable using a floor plan (or other hand-drawn or annotated map)…
▽ More
Maps --- specifically floor plans --- are useful for a variety of tasks from arranging furniture to designating conceptual or functional spaces (e.g., kitchen, walkway). We present a simple algorithm for quickly laying a floor plan (or other conceptual map) onto a SLAM map, creating a one-to-one mapping between them. Our goal was to enable using a floor plan (or other hand-drawn or annotated map) in robotic applications instead of the typical SLAM map created by the robot. We look at two use cases, specifying "no-go" regions within a room and locating objects within a scanned room. Although a user study showed no statistical difference between the two types of maps in terms of performance on this spatial memory task, we argue that floor plans are closer to the mental maps people would naturally draw to characterize spaces.
△ Less
Submitted 15 June, 2016;
originally announced June 2016.
-
Video Manipulation Techniques for the Protection of Privacy in Remote Presence Systems
Authors:
Alexander Hubers,
Emily Andrulis,
Levi Scott,
Tanner Stirrat,
Duc Tran,
Ruonan Zhang,
Ross Sowell,
Cindy Grimm,
William D. Smart
Abstract:
Systems that give control of a mobile robot to a remote user raise privacy concerns about what the remote user can see and do through the robot. We aim to preserve some of that privacy by manipulating the video data that the remote user sees. Through two user studies, we explore the effectiveness of different video manipulation techniques at providing different types of privacy. We simultaneously…
▽ More
Systems that give control of a mobile robot to a remote user raise privacy concerns about what the remote user can see and do through the robot. We aim to preserve some of that privacy by manipulating the video data that the remote user sees. Through two user studies, we explore the effectiveness of different video manipulation techniques at providing different types of privacy. We simultaneously examine task performance in the presence of privacy protection. In the first study, participants were asked to watch a video captured by a robot exploring an office environment and to complete a series of observational tasks under differing video manipulation conditions. Our results show that using manipulations of the video stream can lead to fewer privacy violations for different privacy types. Through a second user study, it was demonstrated that these privacy-protecting techniques were effective without diminishing the task performance of the remote user.
△ Less
Submitted 13 January, 2015;
originally announced January 2015.
