I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.
Q: What is cubical type theory?
A: It’s a type theory giving homotopy type theory its computational meaning.
Q: What is homotopy type theory then?
A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.
The database can make use of a more expressive type system. Specifically to enforce invariants on data integrity at the schema level. But also understanding databases from a type theoretic point of view can lead to better, safer and more expressive type systems.
You do not want to keep writing database validation code in your application boundary. That is tiring. Instead let your database do that work. After all, it is where the data is stored. It is where the data is migrated. So shouldn't it also maintain the integrity and the constraints of the data?
theory Fulcrum | |
imports Main | |
begin | |
(* https://twitter.com/Hillelogram/status/987432184217731073: | |
Fulcrum. Given a sequence of integers, returns the index i that minimizes |sum(seq[..i]) - sum(seq[i..])|. Does this in O(n) time and O(n) memory. https://rise4fun.com/Dafny/S1WMn *) | |
(* The following merely asserts the time and space bounds. *) | |
(* Tail-recursive-modulo-cons calculation of running total - O(n) time and space *) |
module Unify where | |
-- Translated from http://strictlypositive.org/unify.ps.gz | |
open import Data.Empty | |
import Data.Maybe as Maybe | |
open Maybe hiding (map) | |
open import Data.Nat | |
open import Data.Fin | |
open import Data.Product hiding (map) |
# I never knew that singleton methods defined on a class are callable via subclasses | |
# Apparently when you create a subclass, that subclass's singleton class has | |
# its superclass's singleton class as an ancestor. | |
class Foo | |
@blip = 'foo' | |
def self.foo; @blip;end | |
end |
-- Formalization of untyped lambda calculus | |
module 2013-10-23-lambda where | |
open import Level hiding (zero;suc) | |
open import Function using (_∘_;id;_⟨_⟩_) | |
open import Data.Empty | |
open import Data.Star as Star using (Star;_◅_;_◅◅_;ε;_⋆) | |
open import Relation.Binary | |
open import Relation.Binary.PropositionalEquality hiding (subst) | |
open import Data.Product as P hiding (map;zip) |
In fork-join concurrency scenario (here's an example of what the interface may look like)
it may happen that we would want to pass Arc<Mutex<Vec<&mut int>>>
to child threads (you can imagine that instead of int
there's really big structure that parent thread could access only by reference, so I think it's a pretty reasonable scenario).
So we want to wrap Vec<&mut int>
in a Mutex
, but that requires Send
and our vector doesn't fulfill Send
.
So to be able to do that, we may just remove Send
bound from Mutex::new
. We may think that it won't introduce any unsafety,
because Send
or 'static
bound will be checked by spawn
or similar methods anyway.
But unfortunately, now we are able to pass Arc<Mutex<Rc>>
too, which for sure shouldn't be legal, because of internal, non-thread safe, mutability of Rc
.
So my proposed solution is to keep Send
bound for Mutex::new
, but decouple Send
from 'static
. Send
would only mean "has Sync env