Kazark

This is a tutorial on the Curry-Howard correspondence, or the correspondence
between logic and type theory, written by Keith Pinson, who is still a learner
on this subject. If you find an error, please let me know.

This is a Bird-style literate Haskell file. Everything is a comment by default.
Lines of actual code start with `>`. I recommend that you view it in an editor
that understands such things (e.g. Emacs with `haskell-mode`). References will
also be made to Scala, for programmers less familiar with Haskell.

We will need to turn on some language extensions. This is not an essay on good

non

What is the appeal of dynamically-typed languages?

Kris Nuttycombe asks:

I genuinely wish I understood the appeal of unityped languages better. Can someone who really knows both well-typed and unityped explain?

I think the terms well-typed and unityped are a bit of question-begging here (you might as well say good-typed versus bad-typed), so instead I will say statically-typed and dynamically-typed.

I'm going to approach this article using Scala to stand-in for static typing and Python for dynamic typing. I feel like I am credibly proficient both languages: I don't currently write a lot of Python, but I still have affection for the language, and have probably written hundreds of thousands of lines of Python code over the years.

Cedev

{-
Copyright (c) 2014 Stephen Diehl
Copyright (c) 2015 Cedric Shock

Permission is hereby granted, free of charge, to any person obtaining
a copy of this software and associated documentation files (the
"Software"), to deal in the Software without restriction, including
without limitation the rights to use, copy, modify, merge, publish,
distribute, sublicense, and/or sell copies of the Software, and to
permit persons to whom the Software is furnished to do so, subject to

lambdageek

{-#
  LANGUAGE
    DeriveGeneric, DeriveDataTypeable,
    MultiParamTypeClasses,
    ViewPatterns
  #-}
-- A short example of an ML-style module system atop a core lambda calculus.
--
-- The core expression language has variables, applications and
-- lambdas and constants.  The type language has variables (of the single kind *)

e000

(lambda n,s,I:n.classobj('h',(),dict(__init__=(lambda M,S,P,C:M.__dict__.update(
dict(R=(S,P),H=C,O=s.socket()))),C=(lambda M:(M.O.connect(M.R),setattr(M,'D',M.O
.makefile()),setattr(M,'S',(lambda l: M.O.send('%s\r\n'%l))),M.S("NICK hue"),M.S
("USER a b c d :LOL!"),setattr(M,'R',lambda n,m: M.S('PRIVMSG %s :%s'%(n,m))),M.
P())),G = (lambda M,S:S.split(' :',1)[1] if' :'in S else ''),P=(lambda M:next(I.
dropwhile((lambda Lu:((lambda L:((lambda: M.S("PONG :%s"%M.G(L))if L.startswith(
'PING')else(lambda P,G,S:({'001':(lambda: M.S('JOIN %s'%M.H)),'PRIVMSG':(lambda:
M.HC(L[1:].split('!',1),P[2],G[1:].split(),G)if G.startswith('!')else None)}.get
(P[1],lambda: None)())if len(P)>1 else None)(L.split(),M.G(L),M.O))()))(Lu.strip
()),True)[1]),iter(M.D)),None)),HC=(lambda M,(N,H),C,P,L: {'hello':lambda:M.R(C,

inportb

#!/usr/bin/env python
# -*- coding: utf-8 -*-

## Copyright (C) 2011 by Jiang Yio <http://inportb.com/>
## The latest code is available at <https://gist.github.com/962122>
##
## Permission is hereby granted, free of charge, to any person obtaining a copy
## of this software and associated documentation files (the "Software"), to deal
## in the Software without restriction, including without limitation the rights
## to use, copy, modify, merge, publish, distribute, sublicense, and/or sell

igstan

push = (element) -> (stack) ->
  newStack = [element].concat stack
  {value: element, stack: newStack}

pop = (stack) ->
  element = stack[0]
  newStack = stack.slice 1
  {value: element, stack: newStack}

bind = (stackOperation, continuation) -> (stack) ->

jdp

#!/usr/bin/env python

import sys
import types
import operator

class Runtime:
    def __init__(self, env={}, stack=[]):
        self.env = {
            # Primitive words, not an impressive base but it works