CodaFi

/*
 struct G<A> {
  let vertices : [A]
  let edges: [(A, A)]
}

let gex = G(vertices: [1, 2, 3], edges: [(1, 2), (2, 3)])
let gbad = G(vertices: [1], edges: [(1, 2)])
*/

CodaFi

module MonadsAsModules where

import Agda.Primitive using (Level)

id : ∀ {k}{X : Set k} → X → X
id x = x

const : ∀ {a b} {A : Set a} {B : Set b} → A → B → A
const x _ = x

CodaFi

#!/bin/sh

set -e

if [ -z "${SWIFTPM_CONFIGURATION}" ]; then
  SWIFTPM_CONFIGURATION=.bootstrap/lib/swift/pm/4
fi

if [ -z "${CONFIGURATION}" ]; then
    CONFIGURATION=release

CodaFi

// swift -Xfrontend -debug-constraints

infix operator ^&&^ : LogicalConjunctionPrecedence
infix operator ^||^ : LogicalConjunctionPrecedence

struct T{}
struct F{}

func λ(_ f : (T) -> ()) {
  print("true")

CodaFi

indirect enum Type : CustomStringConvertible {
  case TyVar(String)
  case Top
  case Bottom
  case Arrow(Type, Type)
  case Pair(Type, Type)
  case Rec(String, Type)

  func subst(_ s : String, _ t : Type) -> Type {
    switch self {

CodaFi

Explicit Toll-Free Conversions

• Proposal: SE-NNNN
• Authors: Robert Widmann
• Review Manager: TBD
• Status: Awaiting review

Introduction

To continue removing further implicit conversions from the language, implicit toll-free bridging should be deprecated in Swift 3 and removed in Swift 4.0.

CodaFi

/// Playground - noun: a place where people can play
/// An un-parser for things is a continuation on strings...

precedencegroup CompositionPrecedence {
  associativity: right
  higherThan: BitwiseShiftPrecedence
}

prefix operator <<
postfix operator >>

CodaFi

indirect enum Type : CustomStringConvertible {
  case nat
  case product(Type, Type)
  case arrow(Type, Type)

  var description : String {
    switch self {
    case .nat:
      return "ℕ"
    case let .product(t1, t2):

CodaFi

//
//  Channel.swift
//  Sessions
//
//  Created by Robert Widmann on 2/27/17.
//  Copyright © 2017 TypeLift. All rights reserved.
//

enum FakeError : Error {
  case Error

CodaFi

Modular Swift

• Proposal: SE-NNNN
• Authors: Robert Widmann, Jaden Geller
• Review Manager: TBD
• Status: Awaiting review

Introduction