m-alvarez

module type Iter = sig
  type 'a coll
  type 'a t

  val iter : 'a coll -> 'a t
  val next : 'a t -> ('a * 'a t) option
end

module IterLemmas(I : Iter) = struct
  let fold (x: 'a) (f: 'a -> 'b -> 'a) (coll: 'b I.coll) =

m-alvarez

-- type-in-type is unlikely to be necessary, but it does make my life easier.
{-# OPTIONS --type-in-type         #-}

module Scott where

open import Function
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Data.Product
open import Data.Sum

m-alvarez

exception Found_element of int

let find_first (p : int -> bool) (s : int Stream.t) =
  try (
    Stream.iter (fun elt -> if p elt then raise (Found_element elt)) s;
    None
  )
  with
    Found_element elt -> Some elt

m-alvarez

package starfighter.types

sealed abstract class TList
sealed class TNil extends TList
sealed class TCons[A, B <: TList] extends TList

object TList {
  type L[A] = TCons[A, TNil]
  type ::[A, B <: TList] = TCons[A, B] 
}

m-alvarez

import std.stdio;
import std.algorithm;

mixin template VarDecl(T, alias string VarName) {
  mixin (`private T `~VarName~`;`);
  mixin (`T get_`~VarName~`() { return this.`~VarName~`; }`);
  mixin (`void set_`~VarName~`(T value) { this.`~VarName~` = value; }`);
}

class Klass {

m-alvarez

validParentheses = (== 1) . foldl (flip ($)) 1 . map (\case { '(' -> (* 2); ')' -> (`div` 2) })

m-alvarez

(* Dimensional analysis in OCaml, using only Hindley-Milner
   with variance annotations!
   The technique for representing typelevel integers that we use
   here is from the talk "Many Holes in Hindley-Milner", by
   Sam Lindley (http://www.kb.ecei.tohoku.ac.jp/ml2008/slides/lindley.pdf) *)

(* This type needs to be covariant so we can
   generalize one : ('_a, '_a suc) int to ('a, 'a suc) int *)
(* It is also necessary to make it concrete so we don't
   allow circular types such as ( 'a suc as 'a, 'a ) int *)

m-alvarez

module type Type = sig
  module type T
end

module Equality = (struct
  module Eq(Typ:Type)(X:Typ.T)(Y:Typ.T) = struct
    module type T = sig end
  end

  module Eq_refl(Typ:Type)(X:Typ.T) = (struct

m-alvarez

#include <vector>
#include <iostream>

template<typename T, int i>
struct Conditional {
    typedef T Type;
};

template<typename T>
struct Conditional<T, 0>;

m-alvarez

convert: item __std_macros with id 4 rp None
convert: item SearchEngine with id 6 rp None
write_ty_to_tcx(6, SearchEngine)
write_ty_to_tcx(7, std::hashmap::HashMap<~str,~str>)
convert: item __extensions__ with id 16 rp None
write_ty_to_tcx(16, SearchEngine)
ty_of_bare_fn
write_ty_to_tcx(65, extern "Rust" fn() -> ~std::iter::Iterator<std::send_str::SendStr><no-bounds>)
convert: item main with id 67 rp None
ty_of_bare_fn