AndyShiue

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.

DaveCTurner

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 *)

CMCDragonkai

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?

oakes

Contents

• Why care about Rust?
• The Toolchain
• Creating a New Project
• Modules
• Crates
• Types
• References
• Mutability

krdln

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

twanvl

-- 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)

copumpkin

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)

cowboyd

# 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