VictorTaelin

// A nano dependent type-checker featuring inductive types via self encodings.
// All computation rules are justified by interaction combinator semantics,
// resulting in major simplifications and improvements over old Kind-Core.
// Specifically, computable annotations (ANNs) and their counterpart (ANN
// binders) and a new self encoding based on equality (rather than dependent
// motives) greatly reduce code size. A more complete file, including
// superpositions (for optimal unification) is available on the
// Interaction-Type-Theory repository.
// Credits also to Franchu and T6 for insights.

Sgeo

/// This type is only every inhabited when S is nominally equivalent to T
#[derive(Debug)]
pub struct Is<S, T>(::std::marker::PhantomData<(*const S, *const T)>);

// Construct a proof of the fact that a type is nominally equivalent
// to itself.
pub fn is<T>() -> Is<T, T> { Is(::std::marker::PhantomData) }

// std::mem::transmute does not accept unsubstituted type parameters
// manual transmute as suggested by manual

chrisdone

Typing Haskell in Haskell

MARK P. JONES

Pacific Software Research Center

Department of Computer Science and Engineering

Oregon Graduate Institute of Science and Technology

copumpkin

module RuntimeTypes where

open import Function
open import Data.Unit
open import Data.Bool
open import Data.Integer
open import Data.String as String
open import Data.Maybe hiding (All)
open import Data.List
open import Data.List.All

mvr

A Whirlwind Tour of Combinatorial Games in Haskell
==================================================

Combinatorial games are an interesting class of games where two
players take turns to make a move, changing the game from one position
to another. In these games, both players have perfect information
about the state of the game and there is no element of chance. In
'normal play', the winner is declared when the other player is unable
to move. A lot of famous strategy games can be analysed as
combinatorial games: chess, go, tic-tac-toe.

mstewartgallus

/// This type is only every inhabited when S is nominally equivalent to T
pub type Is <S, T> = Is_ <S, T>;

priv struct Is_ <S, T>;

// Construct a proof of the fact that a type is nominally equivalent
// to itself.
pub fn Is <T> () -> Is <T, T> { Is_ }

pub impl <S, T> Is_ <S, T> {

pelle

(use '[datomic.api :only [q db] :as d])

(def uri "datomic:mem://accounts")

;; create database
(d/create-database uri)

;; connect to database
(def conn (d/connect uri))

simonmichael

# unregister broken GHC packages. Run this a few times to resolve dependency rot in installed packages.                                                                                                                                     
# ghc-pkg-clean -f cabal/dev/packages*.conf also works.                                                                                                                                                                                     
function ghc-pkg-clean() {
    for p in `ghc-pkg check $* 2>&1  | grep problems | awk '{print $6}' | sed -e 's/:$//'`
    do
        echo unregistering $p; ghc-pkg $* unregister $p
    done
}

# remove all installed GHC/cabal packages, leaving ~/.cabal binaries and docs in place.                                                                                                                                                     

jolby

(ns tiexample.core)

(defn ^{:export dbg} dbg [s]
  (js* "Titanium.API.debug(~{s})"))

;;stolen from another gist I saw
(defn make-js-map
  "makes a javascript map from a clojure one"
  [cljmap]
  (let [out (js-obj)]