gallais

{-# OPTIONS --copatterns #-}

module UntypedLambda where

open import Size
open import Function

mutual

  data Delay (A : Set) (i : Size) : Set where

igstan

• https://www.mpi-sws.org/~rossberg/papers/Rossberg%20-%20Typed%20Open%20Programming.pdf
• http://www.cis.upenn.edu/~bcpierce/courses/629/papers/Saraswat-javabug.html
• https://books.google.ro/books?id=A5ic1MPTvVsC&pg=PA303&lpg=PA303&dq=type+safety+and+linkers&source=bl&ots=PorxgGbx8y&sig=mRUmqqY4bVhrpmXe8xDMHiwXByE&hl=en&sa=X&ved=0CDcQ6AEwBDgKahUKEwio9LzB99zHAhWFCBoKHb6_CJ8#v=onepage&q=%22language-specific%20linkers%22&f=false
• http://glew.org/nglew/papers/mtal.pdf
• http://www.dmst.aueb.gr/dds/pubs/jrnl/1991-SIGPLAN-CType/html/tsl.pdf
• http://lucacardelli.name/Papers/Linking.pdf
• https://upsilon.cc/~zack/research/publications/jfla10-dh-ocaml.pdf
• http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.142.4305&rep=rep1&type=pdf

paf31

module Main where
  
import Data.Maybe (fromMaybe)

import Control.Applicative
import Control.Arrow (first)
import Control.Monad (ap) 
    
import Debug.Trace
  

karpathy

"""
Minimal character-level Vanilla RNN model. Written by Andrej Karpathy (@karpathy)
BSD License
"""
import numpy as np

# data I/O
data = open('input.txt', 'r').read() # should be simple plain text file
chars = list(set(data))
data_size, vocab_size = len(data), len(chars)

chrisdone

Basic unit type:

λ> replTy "()"
() :: ()

Basic functions:

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

bobatkey

(* This is a demonstration of the use of the SML module system to
   encode (Generalized Algebraic Datatypes) GADTs via Church
   encodings. The basic idea is to use the Church encoding of GADTs in
   System Fomega and translate the System Fomega type into the module
   system. As I demonstrate below, this allows things like the
   singleton type of booleans, and the equality type, to be
   represented.

   This was inspired by Jon Sterling's blog post about encoding proofs
   in the SML module system:

jonsterling

(* It is not possible in Standard ML to construct an identity type (or any other
 * indexed type), but that does not stop us from speculating. We can specify with
 * a signature equality should mean, and then use a functor to say, "If there
 * were a such thing as equality, then we could prove these things with it."
 * Likewise, we can use the same trick to define the booleans and their
 * induction principle at the type-level, and speculate what proofs we could
 * make if we indeed had the booleans and their induction principle.
 *
 * Functions may be defined by asserting their inputs and outputs as
 * propositional equalities in a signature; these "functions" do not compute,

tonymorris

using System;

namespace PureIO {
  /*
    C# does not have proper sum types. They must be emulated.

    This data type is one of 4 possible values:
    - WriteOut, being a pair of a string and A
    - WriteErr, being a pair of a string and A
    - readLine, being a function from string to A