andrejbauer

(* How do to topology in Coq if you are secretly an HOL fan.
   We will not use type classes or canonical structures because they
   count as "advanced" technology. But we will use notations.
 *)

(* We think of subsets as propositional functions.
   Thus, if [A] is a type [x : A] and [U] is a subset of [A],
   [U x] means "[x] is an element of [U]".
*)
Definition P (A : Type) := A -> Prop.

martende

#!/bin/sh
exec scala "$0" "$@"
!#

object HelloWorld {
  
  abstract class OCard {
    val v:Int
    val c:Int
    def matchV(x:OCard):Boolean

emtenet

%% vim:set softtabstop=4 shiftwidth=4 tabstop=4:
-module(sign_certificate).
-author("Michael Taylor <[email protected]>").

%% External exports
-export([sign_certificate/1]).

% sign a certificate from a certificate signing request (CSR)
% RequestDER is a CSR binary in DER format
% return Certificate as binary in DER format

CodaFi

/// Playground - noun: a place where people can play
/// Church-Turing clan ain’t nothing to func with.

/// Church encoding is a means of representing data and operators in the lambda
/// calculus.  In Swift, this means restricting functions to their fully curried
/// forms; returning blocks wherever possible.  Church Encoding of the natural
/// numbers is the most well-known form of encoding, but the lambda calculus is
/// expressive enough to represent booleans, conditionals, pairs, and lists as
/// well.  This file is an exploration of all 4 representations mentioned.

moloneymb

namespace Tsunami.Server

open System
open System.IO
open System.Linq
open System.Net
open System.Net.Sockets
open System.Text
open System.Threading
open System.Runtime.Serialization

sgtz

namespace WebSocket

// Appache 2.0 license

// References:
// [1] Proposed WebSockets Spec December 2011         http://tools.ietf.org/html/rfc6455   
// [2] John McCutchan (Google Dart Team Member)       http://www.altdevblogaday.com/2012/01/23/writing-your-own-websocket-server/
// [3] A pretty good Python implemenation by mrrrgn   https://github.com/mrrrgn/websocket-data-frame-encoder-decoder/blob/master/frame.py
// [4] WebSockets Organising body                     http://www.websocket.org/echo.html
// [5] AndrewNewcomb's Gist (starting point)          https://gist.github.com/AndrewNewcomb/711664

kachayev

Parsing CSS file with monadic parser in Clojure

Inspired by "Parsing CSS with Parsec".

Just quick notes and code that you can play with in REPL.

By @kachayev

0. Intro

rgrinberg

-module(omegle).
-compile(export_all).
-include_lib("n2o/include/wf.hrl").

main() -> #dtl{ file="index", app=nitroshell, bindings=[{body, body()}]}.

body() ->
    {ok, Pid} = wf:async("matcher", fun () -> matcher() end),
    [ #span{ id=status, body="Welcome"}, #br{},
      #span{ id=ui, body=ui(seek, Pid) } ].

tel

Simpler, Easier!

Lennart Augustsson, Oct 25, 2007

In a recent paper, Simply Easy! (An Implementation of a Dependently Typed Lambda Calculus), the authors argue that type checking a dependently typed language is easy. I agree whole-heartedly, it doesn't have to be difficult at all. But I don't think the paper presents the easiest way to do it. So here is my take on how to write a simple dependent type checker. (There's nothing new here, and the authors of the paper are undoubtedly familiar with all of it.)

First, the untyped lambda calculus.

I'll start by implementing the untyped lambda calculus. It's a very simple language with just three constructs: variables, applications, and lambda expressions, i.e.,

zraffer

package object types {

  import scala.language.reflectiveCalls
  import scala.language.higherKinds

  // quantifiers aka (co)ends
  type Forall[+F[_]] = { def apply[X]: F[X] }
  type Exists[+F[_]] = F[_]

  // basic categorical notions