Hindley-Milner type inference over (Lisp-ish) S-expressions

/*
Copyright (c) 2017 Cyril Jandia

http://www.cjandia.com/

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
the following conditions:

The above copyright notice and this permission notice shall be included
in all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED ``AS IS'', WITHOUT WARRANTY OF ANY KIND, EXPRESSED
OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE WARRANTIES OF
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
IN NO EVENT SHALL CYRIL JANDIA BE LIABLE FOR ANY CLAIM, DAMAGES OR
OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
OTHER DEALINGS IN THE SOFTWARE.

Except as contained in this notice, the name of Cyril Jandia shall
not be used in advertising or otherwise to promote the sale, use or
other dealings in this Software without prior written authorization
from Cyril Jandia.

Inquiries : ysharp {dot} design {at} gmail {dot} com
 */
using System;
using System.Collections.Generic;
using System.Linq;
using System.Reflection;
using System.Text;
using System.Text.RegularExpressions;

namespace System.Language.SExpressions
{
    public delegate object Acceptor(Token token, string match);

    public class Symbol
    {
        public Symbol(string id) { Id = id ?? Guid.NewGuid().ToString("P"); }
        public override string ToString() => Id;
        public string Id { get; private set; }
    }

    public class Token : Symbol
    {
        internal Token(string id) : base(id) { }
        public Token(string id, Acceptor acceptor) : this(id, acceptor, false) { }
        public Token(string id, Acceptor acceptor, bool priority) : this(id, id, acceptor, priority) { }
        public Token(string id, string pattern, Acceptor acceptor) : this(id, pattern, acceptor, false) { }
        public Token(string id, string pattern, Acceptor acceptor, bool priority) : base(id) { Regex = new Regex(string.Format("^({0})", !string.IsNullOrEmpty(Pattern = pattern) ? Pattern : ".*"), RegexOptions.Compiled); ValueOf = acceptor; HasPriority = priority; }
        public string Pattern { get; private set; }
        public Regex Regex { get; private set; }
        public Acceptor ValueOf { get; private set; }
        public bool HasPriority { get; private set; }
    }

    public class Syntax
    {
        private static readonly Token Space = Token("s+", Echo, 1);
        private static readonly Token Open = Token("(", Echo);
        private static readonly Token Close = Token(")", Echo);
        private static object Echo(Token token, string match) => new Token(token.Id);
        private Token comment;
        private Token quote;
        private Token @params;
        private Token @this;

        private Tuple Read(ref string input)
        {
            if (!string.IsNullOrEmpty(input))
            {
                var found = null as Match;
                var sofar = input;
                var tuple = Lexicon.FirstOrDefault(current => (found = current.Item2.Regex.Match(sofar)).Success && (found.Length > 0));
                var token = tuple != null ? tuple.Item2 : null;
                var match = token != null ? found.Value : null;
                input = match != null ? input.Substring(match.Length) : input;
                return token != null ? Tuple.Create(token, match, token.ValueOf(token, match)) : null;
            }
            return null;
        }

        private Tuple Next(ref string input)
        {
            Tuple read;
            while (((read = Read(ref input)) != null) && ((read.Item1 == Comment) || (read.Item1 == Space))) ;
            return read;
        }

        public object Parse(ref string input, Tuple next)
        {
            var value = null as object;
            if (next != null)
            {
                var token = next.Item1;
                if (token == Open)
                {
                    var list = new List();
                    while (((next = Next(ref input)) != null) && (next.Item1 != Close))
                    {
                        list.Add(Parse(ref input, next));
                    }
                    if (next == null)
                    {
                        throw Language.Error("unexpected EOF");
                    }
                    value = list.ToArray();
                }
                else if (token == Quote)
                {
                    var quote = next.Item3;
                    next = Next(ref input);
                    if (next == null)
                    {
                        throw Language.Error("unexpected EOF");
                    }
                    value = new[] { quote, Parse(ref input, next) };
                }
                else
                {
                    value = next.Item3;
                }
            }
            else
            {
                throw Language.Error("unexpected EOF");
            }
            return value;
        }

        protected Token TokenOf(Acceptor acceptor)
        {
            var optional = new Acceptor[] { Commenting, Parameters, Self };
            var found = Lexicon.FirstOrDefault(pair => pair.Item2.ValueOf == acceptor);
            var token = found != null ? found.Item2 : null;
            if ((token == null) && !Optional.Contains(acceptor))
            {
                throw Language.Error("missing required token definition: {0}", acceptor.Method.Name);
            }
            return token;
        }

        protected virtual Syntax Validate()
        {
            Required.Select(acceptor => TokenOf(acceptor)).Count();
            return this;
        }

        protected IList> Lexicon { get; private set; }
        protected HashSet Required { get; set; }
        protected HashSet Optional { get; set; }

        public static Symbol Symbol(object value) => value as Symbol;
        public static string Identifier(object value) => Symbol(value) != null ? Symbol(value).Id : null;
        public static string Escape(string pattern) => Escape(pattern, -1);

        public static string Escape(string pattern, int count)
        {
            count = count < 0 ? pattern.Length : count;
            return pattern.Aggregate(new StringBuilder(), (escaped, character) => escaped.AppendFormat("{0}{1}", count-- > 0 ? "\\" : string.Empty, character)).ToString();
        }

        public static object Commenting(Token token, string match) => Echo(token, match);
        public static object NewSymbol(Token token, string match) => new Symbol(match);
        public static object Quoting(Token token, string match) => NewSymbol(token, match);
        public static object Parameters(Token token, string match) => NewSymbol(token, match);
        public static object Self(Token token, string match) => NewSymbol(token, match);
        public static Token Token(string pattern, Acceptor acceptor) => Token(pattern, acceptor, -1);
        public static Token Token(string pattern, Acceptor acceptor, int escapeCount) => Token(pattern, acceptor, escapeCount, false);
        public static Token Token(string pattern, Acceptor acceptor, bool hasPriority) => Token(pattern, acceptor, -1, hasPriority);
        public static Token Token(string pattern, Acceptor acceptor, int escapeCount, bool hasPriority) => new Token(pattern, Escape(pattern, escapeCount), acceptor, hasPriority);
        public static Token Lexical(string pattern, Acceptor acceptor) => Token(pattern, acceptor, 0);
        public static Token Lexical(string pattern, Acceptor acceptor, bool hasPriority) => Token(pattern, acceptor, 0, hasPriority);

        public static string ToString(object value)
        {
            return
                value is object[] ?
                ((object[])value).Length > 0 ? ((object[])value).Aggregate(new StringBuilder("("), (result, obj) => result.AppendFormat(" {0}", ToString(obj))).Append(" )").ToString() : "( )"
                :
                (value != null ? (value is string ? string.Concat('"', (string)value, '"') : (value is bool ? value.ToString().ToLower() : value.ToString())).Replace("\\\r\n", "\r\n").Replace("\\\n", "\n").Replace("\\t", "\t").Replace("\\n", "\n").Replace("\\r", "\r").Replace("\\\"", "\"") : null) ?? "(null)";
        }

        public Syntax()
        {
            Lexicon = new List>();
            Required = new HashSet(new Acceptor[] { NewSymbol, Quoting });
            Optional = new HashSet(new Acceptor[] { Commenting, Parameters, Self });
            Include(Space, Open, Close);
        }

        public Syntax Include(Token token)
        {
            if (Lexicon.FirstOrDefault(pair => pair.Item1 == token.Pattern) == null)
            {
                if (token.HasPriority)
                {
                    Lexicon.Insert(0, Tuple.Create(token.Pattern, token));
                }
                else
                {
                    Lexicon.Add(Tuple.Create(token.Pattern, token));
                }
            }
            return this;
        }

        public Syntax Include(params Token[] tokens) => tokens.Aggregate(this, (syntax, token) => syntax.Include(token));

        public object Parse(string input)
        {
            Validate();
            var next = Next(ref input);
            var value = Parse(ref input, next);
            if ((next = Next(ref input)) != null)
            {
                throw Language.Error("unexpected ", next.Item1);
            }
            return value;
        }

        public Token Comment { get { return comment = comment ?? TokenOf(Commenting); } }
        public Token Quote { get { return quote = quote ?? TokenOf(Quoting); } }
        public Token Params { get { return @params = @params ?? TokenOf(Parameters); } }
        public Token This { get { return @this = @this ?? TokenOf(Self); } }
    }

    public class SemanticAttribute : Attribute
    {
        protected SemanticAttribute(string id) { Id = id; }
        public string Id { get; private set; }
    }

    [AttributeUsage(AttributeTargets.Property | AttributeTargets.Method | AttributeTargets.Field, AllowMultiple = false, Inherited = false)]
    public class BuiltinAttribute : SemanticAttribute
    {
        public BuiltinAttribute(string id) : base(id) { }
    }

    [AttributeUsage(AttributeTargets.Method, AllowMultiple = false, Inherited = false)]
    public class KeywordAttribute : SemanticAttribute
    {
        public KeywordAttribute(string id) : this(id, false) { }
        public KeywordAttribute(string id, bool isInfix) : base(id) { IsInfix = isInfix; }
        public bool IsInfix { get; private set; }
    }

    public class Callable : Symbol
    {
        protected Callable(int length) : this(null, length) { }
        protected Callable(string id, int length) : base(id) { Length = length; }
        protected int Count(object[] arguments) { return arguments != null ? arguments.Length : 0; }
        public virtual object Invoke(params object[] arguments) { throw Language.Error("not implemented"); }
        public Delegate Delegate { get; protected set; }
        public bool Variadic { get; protected set; }
        public int Length { get; private set; }
    }

    public delegate object Semantic(Environment environment, object expression);

    public class Builtin : Callable
    {
        protected Builtin(string id, int length) : base(id, length) { }
    }

    public class Keyword : Builtin
    {
        public Keyword(string id, Semantic semantic) : this(id, semantic, false) { }
        public Keyword(string id, Semantic semantic, bool isInfix) : base(id, -1) { Delegate = semantic; IsInfix = isInfix; }
        public Semantic Semantic { get { return (Semantic)Delegate; } }
        public bool IsInfix { get; private set; }
    }

    public class Builtin : Builtin
    {
        public Builtin(string id, Func function) : base(id, 0) { Delegate = (Function = function); }
        public override object Invoke(params object[] arguments) { var count = Count(arguments); return Function(count > 0 ? (Environment)arguments[0] : null); }
        public Func Function { get; private set; }
    }

    public class Builtin : Builtin
    {
        public Builtin(string id, Func function) : base(id, 1) { Delegate = (Function = function); var arg1 = Function.Method.GetParameters()[1]; Variadic = (typeof(T1) == typeof(object[])) && (arg1.GetCustomAttributes(false).FirstOrDefault(attribute => attribute is ParamArrayAttribute) != null); }
        public override object Invoke(params object[] arguments) { var count = Count(arguments); return Function(count > 0 ? (Environment)arguments[0] : null, count > 1 ? (T1)arguments[1] : default(T1)); }
        public Func Function { get; private set; }
    }

    public class Builtin : Builtin
    {
        public Builtin(string id, Func function) : base(id, 2) { Delegate = (Function = function); }
        public override object Invoke(params object[] arguments) { var count = Count(arguments); return Function(count > 0 ? (Environment)arguments[0] : null, count > 1 ? (T1)arguments[1] : default(T1), count > 2 ? (T2)arguments[2] : default(T2)); }
        public Func Function { get; private set; }
    }

    public class Builtin : Builtin
    {
        public Builtin(string id, Func function) : base(id, 3) { Delegate = (Function = function); }
        public override object Invoke(params object[] arguments) { var count = Count(arguments); return Function(count > 0 ? (Environment)arguments[0] : null, count > 1 ? (T1)arguments[1] : default(T1), count > 2 ? (T2)arguments[2] : default(T2), count > 3 ? (T3)arguments[3] : default(T3)); }
        public Func Function { get; private set; }
    }

    public class Builtin : Builtin
    {
        public Builtin(string id, Func function) : base(id, 4) { Delegate = (Function = function); }
        public override object Invoke(params object[] arguments) { var count = Count(arguments); return Function(count > 0 ? (Environment)arguments[0] : null, count > 1 ? (T1)arguments[1] : default(T1), count > 2 ? (T2)arguments[2] : default(T2), count > 3 ? (T3)arguments[3] : default(T3), count > 4 ? (T4)arguments[4] : default(T4)); }
        public Func Function { get; private set; }
    }

    public class Builtin : Builtin
    {
        public Builtin(string id, Func function) : base(id, 4) { Delegate = (Function = function); }
        public override object Invoke(params object[] arguments) { var count = Count(arguments); return Function(count > 0 ? (Environment)arguments[0] : null, count > 1 ? (T1)arguments[1] : default(T1), count > 2 ? (T2)arguments[2] : default(T2), count > 3 ? (T3)arguments[3] : default(T3), count > 4 ? (T4)arguments[4] : default(T4), count > 5 ? (T5)arguments[5] : default(T5)); }
        public Func Function { get; private set; }
    }

    public class Lambda : Callable
    {
        public Lambda(object definition, Func closure, int length) : base(length) { Definition = definition; Delegate = (Closure = closure); }
        public override string ToString() { var pair = (object[])Definition; return string.Concat(Syntax.ToString(pair[0]), " => ", Syntax.ToString(pair[1])); }
        public override object Invoke(params object[] arguments) { return Closure(arguments); }
        public Func Closure { get; private set; }
        public object Definition { get; private set; }
    }

    public class Environment : Dictionary
    {
        private object[] GetBindings() { var bindings = this.Where(pair => !Equals(pair.Key, string.Empty)).Select(pair => new[] { pair.Key, pair.Value }); var keyed = new HashSet(bindings.Select(pair => pair[0])); var bound = (Outer != null ? Outer.Bindings.Where(pair => !keyed.Contains(((object[])pair)[0])).Concat(bindings) : bindings).ToArray(); return bound; }
        private bool TryGet(string id, ref object value) { if (id != null) { if (!ContainsKey(id)) { return Outer != null ? Outer.TryGet(id, ref value) : false; } else { value = id.Length > 0 ? this[id] : Bindings; return true; } } else return false; }
        private object[] Bindings { get { return GetBindings(); } }
        public Environment(Language evaluator, Environment outer) : this(evaluator, null as IDictionary) { Outer = outer; }
        public Environment(Language evaluator, IDictionary builtins) { Language = evaluator; if (builtins != null) { builtins.Aggregate(this, (scope, pair) => { scope.Add(pair.Key, pair.Value); return scope; }); } }
        public object Invoke(string id, params object[] arguments) { return Invoke(Get(id), arguments); }
        public object Invoke(object target, params object[] arguments) { var callable = Language.Require(target as Callable); var argv = new object[arguments != null ? arguments.Length + 1 : 1]; var argc = argv.Length; if (argc > 1) { Array.Copy(arguments, 0, argv, 1, argc - 1); } argv[0] = this; return callable.Invoke(argv); }
        public object Get(string id) { object value = null; if (!TryGet(id, ref value)) { throw Language.Error("undefined {0}", Syntax.ToString(id)); } return value; }
        public bool Knows(Symbol symbol) { object value = null; return TryGet(Language.Require(symbol).Id, ref value); }
        public Language Language { get; private set; }
        public Environment Outer { get; private set; }
        public IDictionary Bound { get { return Bindings.Cast().ToDictionary(binding => (string)binding[0], binding => binding[1]); } }
    }

    public delegate object Evaluator(Environment environment, object expression);

    public class Language
    {
        private Keyword eval;
        private Keyword apply;
        private Keyword quote;
        private Keyword cons;
        private Keyword let;
        private Keyword lambda;
        private Keyword test;

        private Type[] GetSignature(MethodInfo method)
        {
            var parameters = method.GetParameters();
            var length = parameters.Length;
            return parameters.Select(parameter => parameter.ParameterType).Concat(new[] { method.ReturnType }).ToArray();
        }

        private Type GetDelegateType(Type[] signature)
        {
            var delegateTypes = new[] { null, typeof(Func<,>), typeof(Func<,,>), typeof(Func<,,,>), typeof(Func<,,,,>), typeof(Func<,,,,,>), typeof(Func<,,,,,,>) };
            return delegateTypes[signature.Length - 1].MakeGenericType(signature);
        }

        private Type GetBuiltinType(Type[] signature)
        {
            var builtinTypes = new[] { null, typeof(Builtin<>), typeof(Builtin<,>), typeof(Builtin<,,>), typeof(Builtin<,,,>), typeof(Builtin<,,,,>), typeof(Builtin<,,,,,>) };
            return builtinTypes[signature.Length - 1].MakeGenericType(signature.Skip(1).ToArray());
        }

        private IDictionary GetReflectedSemantics()
        {
            return
                GetType().
                GetMembers().
                Aggregate
                (
                    new Dictionary(),
                    (reflected, member) =>
                    {
                        var attribute = member.GetCustomAttribute(false);
                        string id;
                        if ((attribute != null) && ((id = attribute.Id) != null))
                        {
                            var property = member as PropertyInfo;
                            var method = member as MethodInfo;
                            var field = member as FieldInfo;
                            object semantic;
                            if (property != null)
                            {
                                if ((property.GetSetMethod() == null) || !property.GetSetMethod().IsPublic)
                                {
                                    semantic = property.GetValue(this);
                                }
                                else
                                {
                                    throw Error("semantic definition property {0} must be read-only", property.Name);
                                }
                            }
                            else if (method != null)
                            {
                                if (attribute is BuiltinAttribute)
                                {
                                    var signature = GetSignature(method);
                                    var delegateType = GetDelegateType(signature);
                                    var builtinType = GetBuiltinType(signature);
                                    var @delegate = Delegate.CreateDelegate(delegateType, this, method);
                                    semantic = Activator.CreateInstance(builtinType, id, @delegate);
                                }
                                else if (attribute is KeywordAttribute)
                                {
                                    var isInfix = ((KeywordAttribute)attribute).IsInfix;
                                    semantic = Activator.CreateInstance(typeof(Keyword), id, Delegate.CreateDelegate(typeof(Semantic), this, method), isInfix);
                                }
                                else
                                {
                                    throw Error("unsupported semantic definition attribute {0}", attribute.GetType());
                                }
                            }
                            else
                            {
                                if (field.IsInitOnly)
                                {
                                    semantic = field.GetValue(this);
                                }
                                else
                                {
                                    throw Error("semantic definition field {0} must be read-only", field.Name);
                                }
                            }
                            AddSemantic(reflected, id, semantic);
                        }
                        return reflected;
                    }
                );
        }

        internal void AddSemantic(IDictionary semantics, string id, object semantic) => semantics.Add(id, semantic);

        protected Keyword KeywordOf(Semantic semantic)
        {
            var defined = Require(semantic);
            var keyword = Semantics.Values.FirstOrDefault(builtin => (builtin is Keyword) && Equals(((Keyword)builtin).Semantic, defined)) as Keyword;
            if (keyword == null)
            {
                throw Error("missing reserved keyword definition: {0}", defined.Method.Name);
            }
            return keyword;
        }

        protected virtual Language Validate()
        {
            Reserved.Where(semantic => semantic != Evaluation).Select(semantic => KeywordOf(semantic)).Count();
            return this;
        }

        protected virtual object Evaluation(Environment environment, object expression, bool topLevel)
        {
            var list = expression as object[];
            var symbol = Syntax.Symbol(expression);
            if (environment == null)
            {
                return Validate().Evaluation(new Environment(this, Semantics), expression);
            }
            else if (list != null)
            {
                Keyword keyword;
                if ((list.Length > 1) && ((symbol = Syntax.Symbol(list[1])) != null) && ((keyword = Keyword(symbol.Id)) != null))
                {
                    if (keyword.IsInfix)
                    {
                        var head = Syntax.Symbol(list[0]);
                        var lead = head != null ? Keyword(head.Id) : null;
                        if ((lead == null) || !IsReserved(lead))
                        {
                            return keyword.Semantic(environment, new[] { list[0] }.Concat(list.Skip(2)).ToArray());
                        }
                        throw Error("infix keyword {0} not allowed after reserved keyword {1}", keyword, lead);
                    }
                    throw Error("not an infix keyword at position 2: {0}", keyword);
                }
                if ((list.Length > 0) && ((symbol = Syntax.Symbol(list[0])) != null) && ((keyword = Keyword(symbol.Id)) != null))
                {
                    return keyword.Semantic(environment, list.Skip(1).ToArray());
                }
                else
                {
                    int length;
                    list = list.Select(item => Evaluation(environment, item)).ToArray();
                    if (((length = list.Length) > 0) && ((symbol = Syntax.Symbol(list[0])) != null) && (symbol is Callable))
                    {
                        var callable = (Callable)symbol;
                        var variadic = callable.Variadic;
                        var arguments = new object[variadic ? length - 1 : length];
                        if (length > 1)
                        {
                            Array.Copy(list, 1, arguments, variadic ? 0 : 1, length - 1);
                        }
                        if (variadic)
                        {
                            return callable.Invoke(environment, arguments);
                        }
                        else
                        {
                            arguments[0] = environment;
                            return callable.Invoke(arguments);
                        }
                    }
                    else
                    {
                        return list;
                    }
                }
            }
            else if (symbol != null)
            {
                return (Delegator != null ? Delegator(environment, symbol) : null) ?? environment.Get(symbol.Id);
            }
            else
            {
                return (Delegator != null ? Delegator(environment, expression) : null) ?? expression;
            }
        }

        protected bool IsReserved(Keyword keyword) => Reserved.Contains(keyword.Semantic);
        protected IDictionary Semantics { get; private set; }
        protected HashSet Reserved { get; set; }
        protected Keyword Eval { get { return eval = eval ?? KeywordOf(Evaluate); } }
        protected Keyword Apply { get { return apply = apply ?? KeywordOf(Application); } }
        protected Keyword Quote { get { return quote = quote ?? KeywordOf(Quoting); } }
        protected Keyword Cons { get { return cons = cons ?? KeywordOf(Construction); } }
        protected Keyword Let { get { return let = let ?? KeywordOf(Letting); } }
        protected Keyword Lambda { get { return lambda = lambda ?? KeywordOf(Abstraction); } }
        protected Keyword Test { get { return test = test ?? KeywordOf(Testing); } }

        public static T Require(T value)
            where T : class
        {
            if (value != null)
            {
                return value;
            }
            throw Error("value must be a {0}", typeof(T));
        }

        public static KeyValuePair Keyword(string id, Semantic semantic) => Keyword(id, semantic, false);
        public static KeyValuePair Keyword(string id, Semantic semantic, bool isInfix) => new KeyValuePair(id, new Keyword(id, semantic, isInfix));
        public static KeyValuePair Builtin(string id, object value) => new KeyValuePair(id, value);
        public static KeyValuePair Builtin(string id, Func function) => new KeyValuePair(id, new Builtin(id, function));
        public static KeyValuePair Builtin(string id, Func function) => new KeyValuePair(id, new Builtin(id, function));
        public static KeyValuePair Builtin(string id, Func function) => new KeyValuePair(id, new Builtin(id, function));
        public static KeyValuePair Builtin(string id, Func function) => new KeyValuePair(id, new Builtin(id, function));
        public static KeyValuePair Builtin(string id, Func function) => new KeyValuePair(id, new Builtin(id, function));
        public static KeyValuePair Builtin(string id, Func function) => new KeyValuePair(id, new Builtin(id, function));
        public static Exception Error(string message, params object[] arguments) => new Exception(string.Format(message, arguments));

        public Language()
            : this(null)
        {
        }

        public Language(Syntax syntax)
        {
            Syntax = syntax ?? new Syntax();
            Semantics = new Dictionary(GetReflectedSemantics());
            Reserved = new HashSet(new Semantic[] { Evaluation, Application, Quoting, Construction, Letting, Abstraction, Testing });
        }

        public Keyword Keyword(string token) => Semantics.ContainsKey(token) ? Semantics[token] as Keyword : null;
        public Language Include(params KeyValuePair[] semanticDefinitions) => semanticDefinitions.Aggregate(this, (language, semanticDefinition) => { language.AddSemantic(Semantics, semanticDefinition.Key, semanticDefinition.Value); return language; });

        public object Evaluate(string input) => Evaluate(null as Environment, new object[] { input });
        public object Evaluate(string input, params object[] arguments) => Evaluate((arguments != null) && (arguments.Length > 0) ? string.Format(input, arguments) : input);
        public object Evaluate(Environment environment, object expression) => Evaluation(environment, Syntax.Parse((string)(expression as object[])[0]), true);

        public object Evaluation(Environment environment, object expression) => Evaluation(environment, expression, false);

        public object Application(Environment environment, object expression)
        {
            var list = Require(expression as object[]);
            if (list.Length == 2)
            {
                return Evaluation(environment, new[] { list[0] }.Concat(Evaluation(environment, list[1]) as object[]).ToArray());
            }
            throw Error("list must be a pair");
        }

        public object Quoting(Environment environment, object expression)
        {
            var list = Require(expression as object[]);
            if (list.Length == 1)
            {
                return list[0];
            }
            throw Error("list must be a singleton");
        }

        public object Construction(Environment environment, object expression)
        {
            var list = Require(expression as object[]);
            if (list.Length == 2)
            {
                return new[] { Evaluation(environment, list[0]) }.Concat(Require(Evaluation(environment, list[1]) as object[])).ToArray();
            }
            throw Error("list must be a pair");
        }

        public object Letting(Environment environment, object expression)
        {
            var list = Require(expression as object[]);
            if (list.Length == 2)
            {
                var inner = new Environment(this, environment);
                var assignments = Require(list[0] as object[]);
                for (var i = 0; i < assignments.Length; i++)
                {
                    var assignment = Require(assignments[i] as object[]);
                    if (assignment.Length == 2)
                    {
                        var symbol = Require(assignment[0] as Symbol);
                        var maybeReserved = Keyword(symbol.Id);
                        if ((maybeReserved != null) && IsReserved(maybeReserved))
                        {
                            throw Error("cannot overload reserved keyword: {0}", maybeReserved);
                        }
                        inner[symbol.Id] = Evaluation(environment, assignment[1]);
                    }
                    else
                    {
                        throw Error("list must be a pair");
                    }
                }
                return Evaluation(inner, list[1]);
            }
            throw Error("list must be a pair");
        }

        public object Abstraction(Environment environment, object expression)
        {
            var list = Require(expression as object[]);
            var @params = Syntax.Params;
            var @this = Syntax.This;
            if (list.Length == 2)
            {
                var definition = (object[])list.Clone();
                var arguments = Require(list[0] as object[]);
                var length = arguments.Length;
                var formals = new Symbol[length];
                for (var i = 0; i < length; i++)
                {
                    formals[i] = Require(arguments[i] as Symbol);
                }
                var lambda = null as Lambda;
                lambda =
                    new Lambda
                    (
                        definition,
                        delegate (object[] args)
                        {
                            var inner = new Environment(this, environment);
                            var count = Require(args).Length;
                            var i = 0;
                            if (count > 0)
                            {
                                while (i < length)
                                {
                                    var formal = formals[i++];
                                    if (i < count)
                                    {
                                        inner[formal.Id] = args[i];
                                    }
                                }
                                if (@params != null)
                                {
                                    inner[@params.Id] = args.Skip(1).ToArray();
                                }
                                if (@this != null)
                                {
                                    inner[@this.Id] = lambda;
                                }
                                inner[lambda.Id] = lambda;
                                return Evaluation(inner, definition[1]);
                            }
                            throw Error("invalid invocation");
                        },
                        length
                    );
                return lambda;
            }
            throw Error("list must be a pair");
        }

        public object Testing(Environment environment, object expression)
        {
            var list = Require(expression as object[]);
            if (list.Length == 3)
            {
                return (bool)Evaluation(environment, list[0]) ? Evaluation(environment, list[1]) : Evaluation(environment, list[2]);
            }
            else if (list.Length == 2)
            {
                return Evaluation(environment, new[] { Test, new[] { Test, list[0] }, list[0], list[1] });
            }
            else if (list.Length == 1)
            {
                return environment.Knows(Require(list[0] as Symbol));
            }
            else
            {
                throw Error("list must be a singleton, a pair, or a triple");
            }
        }

        public Evaluator Delegator { get; protected set; }
        public Syntax Syntax { get; private set; }
    }
}

namespace System.Language.TypeInference
{
    #region Abstract syntax tree
    public abstract class Node
    {
        public static Const Const(object value) => new Const { Spec = value != null ? (!(value is IType) ? value.GetType().FullName : value) : typeof(void).FullName };
        public static Var Var(string name) => Var(name, null);
        public static Var Var(string name, object type) => new Var { Spec = name, Type = type };
        public static Apply Apply(Node expr, Node[] args) => Apply(expr, args, null);
        public static Apply Apply(Node expr, Node[] args, bool isAnnotation) => Apply(expr, args, null, isAnnotation);
        public static Apply Apply(Node expr, Node[] args, object ctor) => Apply(expr, args, ctor, false);
        public static Apply Apply(Node expr, Node[] args, object ctor, bool isAnnotation) => new Apply { Spec = expr, Args = args, Type = ctor, IsAnnotation = isAnnotation };
        public static Abstract Abstract(Node[] args, Node body) => Abstract(args, null, body);
        public static Abstract Abstract(Node[] args, object type, Node body) => new Abstract { Args = args, Body = body, Type = type };
        public static Define Define(Var var, Node body) => new Define { Spec = var, Body = (body as Node) ?? Const(body) };
        public static Let Let(Define[] defs, Node body) => new Let { Args = defs, Body = body };
        public abstract IType Infer(ITypeSystem system, IEnvironment env, IList types);
        public object Spec { get; private set; }
        public Node[] Args { get; private set; }
        public Node Body { get; private set; }
        public object Type { get; private set; }
        public bool IsAnnotation { get; private set; }
    }

    public class Const : Node
    {
        public override string ToString() => string.Concat("{", Spec, "}");
        public override IType Infer(ITypeSystem system, IEnvironment env, IList types) => !(Spec is IType) ? system.Const(env, (string)Spec) : (IType)Spec;
    }

    public class Var : Node
    {
        public override string ToString() => Id;
        public override IType Infer(ITypeSystem system, IEnvironment env, IList types) => system.Fresh(env[Id], types.ToArray());
        public string Id => (string)Spec;
        public bool IsConstructor => (Type is IType) && ((IType)Type).IsConstructor;
    }

    public class Abstract : Node
    {
        public override string ToString() => string.Format("( {0}){2} => {1}", Args.Length > 0 ? string.Concat(string.Join(" ", Args.Select(arg => arg.ToString()).ToArray()), " ") : string.Empty, Body, Type != null ? string.Concat(" : ", Type) : string.Empty);
        public override IType Infer(ITypeSystem system, IEnvironment env, IList types)
        {
            var scope = env.Local(system);
            var known = new List(types);
            var args = new List();
            foreach (var arg in Args)
            {
                IType type;
                Var var;
                if (!(arg is Define))
                {
                    var = (Var)arg;
                    if (var.Type != null)
                    {
                        type = !(var.Type is IType) ? system.Const(scope, (string)var.Type) : (IType)var.Type;
                    }
                    else
                    {
                        type = system.NewGeneric();
                        known.Add(type);
                    }
                    scope[var.Id] = type;
                }
                else
                {
                    var spec = ((Define)arg).Body;
                    var = (Var)((Define)arg).Spec;
                    type = system.NewGeneric();
                    system.Unify(type, system.Infer(scope, spec, known));
                    scope[var.Id] = type;
                    known.Add(type);
                }
                args.Add(type);
                if (!type.Value.IsConstructor)
                {
                    type.Value.Bind(var.Id);
                }
            }
            args.Add(system.Infer(scope, Body is Let ? Body.Args[Body.Args.Length - 1] : Body, known));
            if (Type != null)
            {
                system.Unify(args[args.Count - 1], !(Type is IType) ? system.Const(scope, (string)Type) : (IType)Type);
            }
            return system.NewType(TypeSystem.Function, args.ToArray());
        }
    }

    public class Apply : Node
    {
        private bool IsFunction(IType type) => type != null ? (type.Constructor != null ? type.Constructor == TypeSystem.Function : IsFunction(type.Self)) : false;
        private Node ToFormal(ITypeSystem system, IEnvironment env, IList types, Node arg)
        {
            Func typed =
                var =>
                    IsAnnotation && !env.ContainsKey(var.Id) ? env[var.Id] = system.NewGeneric() : env[var.Id];
            var formal =
                IsAnnotation ?
                (
                    arg is Apply ?
                    Define((Var)arg.Args[0], Const(system.Infer(env, (Node)arg.Spec, types)))
                    :
                    arg is Var ? Define((Var)arg, Const(typed((Var)arg))) : arg
                )
                :
                arg is Var ? Define((Var)arg, Const(typed((Var)arg))) : arg;
            return formal;
        }
        private IType AsAnnotationType(ITypeSystem system, IEnvironment env, IList types)
        {
            IType ctor;
            if
            (
                (Spec is Node) &&
                (((ctor = ((Node)Spec).Type as IType)) != null) &&
                (!IsFunction(ctor) || IsAnnotation)
            )
            {
                Args.Select
                    (
                        (arg, i) =>
                            arg is Var ?
                            system.Infer(env, Define((Var)arg, Const(ctor[i])), types)
                            :
                            null
                    ).
                    ToArray();
                var type = system.NewType(ctor, Args.Select(arg => system.Infer(env, ToFormal(system, env, types, arg), types)).ToArray());
                return type;
            }
            else
            {
                return null;
            }
        }
        public override string ToString() => string.Format("( {0} {1})", Spec, Args.Length > 0 ? string.Concat(string.Join(" ", Args.Select(arg => arg.ToString()).ToArray()), " ") : string.Empty);
        public override IType Infer(ITypeSystem system, IEnvironment env, IList types)
        {
            if (Type == null)
            {
                var annotation = AsAnnotationType(system, env, types);
                if (annotation != null)
                {
                    return annotation;
                }
            }
            var args = Args.Select(arg => system.Infer(env, ToFormal(system, env, types, arg), types)).ToList();
            var expr = (Node)Spec;
            var self = system.Infer(env, expr, types);
            IType @out;
            if (Type != null)
            {
                var ctor = !(Type is IType) ? system.Const(env, (string)Type) : (IType)Type;
                @out = system.Infer(env, Apply(Var(ctor.Id, ctor), args.Select(arg => Const(arg)).ToArray(), IsAnnotation), types);
            }
            else
            {
                @out = system.NewGeneric();
                args.Add(@out);
                system.Unify(system.NewType(TypeSystem.Function, args.ToArray()), self);
            }
            return @out;
        }
    }

    public class Define : Node
    {
        public override string ToString() => string.Format("( {0} = {1} )", Spec, Body);
        public override IType Infer(ITypeSystem system, IEnvironment env, IList types)
        {
            var known = new List(types);
            var type = system.NewGeneric();
            var var = (Var)Spec;
            var scope = Body.IsAnnotation ? env.Local(system) : env;
            env[var.Id] = type;
            known.Add(type);
            system.Unify(type, system.Infer(scope, Body, known));
            return env[var.Id] = !type.Value.IsConstructor ? type.Value.Bind(var.Id) : type.Value;
        }
    }

    public class Let : Node
    {
        public override string ToString() => string.Format("( ( {0}) {1} )", Args.Length > 0 ? string.Concat(string.Join(" ", Args.Select(arg => arg.ToString()).ToArray()), " ") : string.Empty, Body);
        public override IType Infer(ITypeSystem system, IEnvironment env, IList types)
        {
            env = env.Local(system);
            return Args.Select(define => system.Infer(env, define, types)).Concat(new[] { system.Infer(env, Body, types) }).Last();
        }
    }
    #endregion

    #region Type schemes
    public interface IType
    {
        IType Bind(string name);
        IType Constructor { get; }
        string Id { get; }
        IType[] Args { get; }
        IType Self { get; }
        Var Name { get; }
        IType Value { get; }
        bool IsConstructor { get; }
        object Metadata { get; }
        IType this[int index] { get; }
    }
    #endregion

    #region Environment
    public interface IEnvironment : IDictionary
    {
        IEnvironment Local(ITypeSystem system);
    }

    public class Environment : Dictionary, IEnvironment
    {
        protected virtual IType Get(string id)
        {
            if (id == null)
            {
                throw new ArgumentNullException("id", "cannot be null");
            }
            if (!ContainsKey(id))
            {
                throw new InvalidOperationException(string.Format("undefined {0}", id));
            }
            return base[id];
        }
        protected virtual void Set(string id, IType type)
        {
            if (id == null)
            {
                throw new ArgumentNullException("id", "cannot be null");
            }
            base[id] = type;
        }

        public Environment() : this(null) { }
        public Environment(IDictionary outer) : base(outer ?? new Dictionary()) { }
        public IEnvironment Local(ITypeSystem system) => system.NewEnvironment(this);
        public new IType this[string id] { get { return Get(id); } set { Set(id, value); } }
    }
    #endregion

    #region Type system
    public interface ITypeSystem
    {
        IEnvironment NewEnvironment();
        IEnvironment NewEnvironment(IDictionary outer);
        IType Fresh(IType t, IType[] types);
        IType Const(IEnvironment env, string ctor);
        IType NewGeneric();
        IType NewType(string id, IType[] args);
        IType NewType(string id, IType[] args, object meta);
        IType NewType(IType constructor, IType[] args);
        IType NewType(IType constructor, IType[] args, object meta);
        IType NewType(IType constructor, string id, IType[] args);
        IType NewType(IType constructor, string id, IType[] args, object meta);
        void Unify(IType t, IType s);
        IType Infer(IEnvironment env, Node node);
        IType Infer(IEnvironment env, Node node, IList types);
    }

    public class TypeSystem : ITypeSystem
    {
        internal abstract class Scheme : IType
        {
            protected Scheme(string id) { if ((this is Type) && (id == null)) { throw new ArgumentNullException("id", "cannot be null"); } Bind(Id = id); }
            protected Scheme(string id, IType[] args) : this(id) { Args = args ?? new IType[0]; }
            public override string ToString() => Id;
            public IType Bind(string name) { Name = Node.Var(name, this); return this; }
            public IType Constructor { get; protected set; }
            public virtual string Id { get; protected set; }
            public IType[] Args { get; private set; }
            public IType Self { get; internal set; }
            public Var Name { get; private set; }
            public IType Value => Self != null ? Self.Value : this;
            public bool IsConstructor => Constructor == this;
            public object Metadata { get; protected set; }
            public IType this[int index] => Args[index];
        }

        internal class Generic : Scheme
        {
            private string alpha;
            private string Alpha() { var id = Uid; var sb = new StringBuilder(); while (id-- > 0) { var r = id % 26; var c = (char)(r + 97); sb.Insert(0, c); id = (id - r) / 26; } return sb.ToString(); }
            private string GetName() => Self != null ? Self.Id : string.Concat('`', alpha ?? (alpha = Alpha()));
            internal Generic(TypeSystem system) : base(null) { Uid = system.NewId(); }
            internal readonly int Uid;
            public override string ToString() => Self != null ? Self.ToString() : base.ToString();
            public override string Id { get { return GetName(); } protected set { } }
        }

        internal class Type : Scheme
        {
            internal Type(IType constructor, string id, IType[] args, object meta) : base(id, args) { Constructor = constructor ?? this; Metadata = meta; }
            public override string ToString() { var id = Args.Length > 0 ? Id : base.ToString(); return (Args.Length > 0 ? string.Format("{0}<{1}>", id, string.Concat(string.Join(", ", Args.Take(Args.Length - 1).Select(arg => arg.ToString())), (Args.Length > 1 ? ", " : string.Empty), Args[Args.Length - 1].ToString())) : id); }
        }

        private static IType Create(IType constructor, string id, IType[] args, object meta) => new Type(constructor, id, args, meta);
        private static IType Prune(IType t)
        {
            Generic var = t as Generic;
            return (var != null) && (var.Self != null) ? (var.Self = Prune(var.Self)) : t;
        }
        private static bool OccursIn(IType t, IType s) => ((s = Prune(s)) != t) ? (s is Type ? OccursIn(t, s.Args) : false) : true;
        private static bool OccursIn(IType t, IType[] types) => types.Any(type => OccursIn(t, type));
        private IType Fresh(IType t, IType[] types, IDictionary vars)
        {
            vars = vars ?? new Dictionary();
            t = Prune(t);
            var var = t as Generic;
            var type = t as Type;
            if (var != null)
            {
                if (!OccursIn(t, types))
                {
                    if (!vars.ContainsKey(var.Uid))
                    {
                        vars[var.Uid] = NewGeneric();
                    }
                    return vars[var.Uid];
                }
                else
                {
                    return t;
                }
            }
            else if (type != null)
            {
                return NewType(type.Constructor, type.Id, type.Args.Select(arg => Fresh(arg, types, vars)).ToArray());
            }
            else
            {
                throw new InvalidOperationException(string.Format("unsupported {0}", t.GetType()));
            }
        }
        private int id;
        internal int NewId() => ++id;

        public static readonly IType Function = Create(null, "Func", null, null);

        #region ITypeSystem
        public virtual IEnvironment NewEnvironment() => NewEnvironment(null);
        public virtual IEnvironment NewEnvironment(IDictionary outer) => new Environment(outer);
        public IType Fresh(IType t, IType[] types) => Fresh(t, types, null);
        public IType Const(IEnvironment env, string ctor) => env[ctor];
        public IType NewGeneric() => new Generic(this);
        public IType NewType(string id, IType[] args) => NewType(id, args, null);
        public IType NewType(string id, IType[] args, object meta) => NewType(null, id, args, meta);
        public IType NewType(IType constructor, IType[] args) => NewType(constructor, args, null);
        public IType NewType(IType constructor, IType[] args, object meta) => NewType(constructor, constructor.Id, args, meta);
        public IType NewType(IType constructor, string id, IType[] args) => NewType(constructor, id, args, null);
        public IType NewType(IType constructor, string id, IType[] args, object meta) => Create(constructor, id, args, meta);
        public void Unify(IType t, IType s)
        {
            t = Prune(t);
            s = Prune(s);
            if (t is Generic)
            {
                if (t != s)
                {
                    if (OccursIn(t, s))
                    {
                        throw new InvalidOperationException(string.Format("recursive unification of {0} in {1}", t, s));
                    }
                    ((Generic)t).Self = s;
                }
            }
            else if ((t is Type) && (s is Generic))
            {
                Unify(s, t);
            }
            else if ((t is Type) && (s is Type))
            {
                var t_type = (Type)t;
                var s_type = (Type)s;
                if ((t_type.Constructor.Id != s_type.Constructor.Id) || (t_type.Args.Length != s_type.Args.Length))
                {
                    throw new InvalidOperationException(string.Format("{0} incompatible with {1}", t_type, s_type));
                }
                for (var i = 0; i < t_type.Args.Length; i++)
                {
                    Unify(t_type.Args[i], s_type.Args[i]);
                }
            }
            else
            {
                throw new InvalidOperationException(string.Format("undecided unification for {0} and {1}", t, s));
            }
        }
        public IType Infer(IEnvironment env, Node node) => Infer(env, node, null);
        public IType Infer(IEnvironment env, Node node, IList types) => node.Infer(this, env, types ?? new List());
        #endregion
    }
    #endregion
}

namespace Test
{
    using System.Language.SExpressions;
    using System.Language.TypeInference;
    
    class Program
    {
        public class CtorInfo
        {
            public readonly string Cons;
            public readonly int Arity;
            public CtorInfo(string cons, int arity) { Cons = cons; Arity = arity; }
            public IType GetType(IEnvironment env) =>
                env.
                Values.
                FirstOrDefault
                (
                    type =>
                        (type.Metadata != null) &&
                        (((CtorInfo)type.Metadata).Cons == Cons) &&
                        (
                            (((CtorInfo)type.Metadata).Arity == Arity) ||
                            (((CtorInfo)type.Metadata).Arity < 0) ||
                            (Arity < 0)
                        )
                );
        }

        static void Main(string[] args)
        {
            var syntax =
                new Syntax().
                Include
                (
                    // Required
                    Syntax.Lexical("'", Syntax.Quoting),

                    // Not-quite-Lisp-indeed; just stolen from our host, C#, as-is
                    Syntax.Lexical("\\/\\/.*", Syntax.Commenting),
                    Syntax.Lexical("false", (token, match) => false),
                    Syntax.Lexical("true", (token, match) => true),
                    Syntax.Lexical("null", (token, match) => null),

                    // Integers (unsigned)
                    Syntax.Lexical("[0-9]+", (token, match) => int.Parse(match)),

                    // String literals
                    Syntax.Lexical("\\\"(\\\\\\n|\\\\t|\\\\n|\\\\r|\\\\\\\"|[^\\\"])*\\\"", (token, match) => match.Substring(1, match.Length - 2)),

                    // For identifiers...
                    Syntax.Lexical("[\\$_A-Za-z][\\$_0-9A-Za-z\\-\\.\\`]*", Syntax.NewSymbol),

                    // ... and such
                    Syntax.Lexical("[\\!\\&\\|\\<\\=\\>\\+\\-\\*\\/\\%\\,\\:@]", Syntax.NewSymbol),
                    Syntax.Lexical("\\&\\&", Syntax.NewSymbol, true),
                    Syntax.Lexical("\\|\\|", Syntax.NewSymbol, true),
                    Syntax.Lexical("\\<\\=", Syntax.NewSymbol, true),
                    Syntax.Lexical("\\>\\=", Syntax.NewSymbol, true),
                    Syntax.Lexical("\\!\\=", Syntax.NewSymbol, true),
                    Syntax.Lexical("\\=\\=", Syntax.NewSymbol, true),
                    Syntax.Lexical("\\=\\>", Syntax.NewSymbol, true),
                    Syntax.Lexical("\\-\\>", Syntax.NewSymbol, true)
                );

            var system = new TypeSystem();
            var env = system.NewEnvironment();

            // Classic
            var @bool = system.NewType(typeof(bool).FullName, null);
            var @int = system.NewType(typeof(int).FullName, null);
            var @string = system.NewType(typeof(string).FullName, null);

            var SignatureType = system.NewType(TypeSystem.Function, null, new CtorInfo("->", -1));

            // Generic list type of some `item' type : List;
            // syntax for lists:
            //  ::= '('  ':'  ')' | '(' ')'
            // (where "( )" is the empty list)
            var ListType = system.NewType("List", new[] { system.NewGeneric() }, new CtorInfo(":", 2));

            // Generic tuple types of some `item1', `item2', ... types : Tuple
            // syntax for tuples:
            //  ::= '('  ',' ... ')' | '(' ',' ')'
            // (where "( , )" is the empty tuple and "( ,  )" or "(  , )" the unary tuple)
            var Tuple00Type = system.NewType("Tuple`0", null, new CtorInfo(",", 0));
            var Tuple01Type = system.NewType("Tuple`1", new[] { system.NewGeneric() }, new CtorInfo(",", 1));
            var Tuple02Type = system.NewType("Tuple`2", new[] { system.NewGeneric(), system.NewGeneric() }, new CtorInfo(",", 2));
            var Tuple03Type = system.NewType("Tuple`3", new[] { system.NewGeneric(), system.NewGeneric(), system.NewGeneric() }, new CtorInfo(",", 3));
            var Tuple04Type = system.NewType("Tuple`4", new[] { system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric() }, new CtorInfo(",", 4));
            var Tuple05Type = system.NewType("Tuple`5", new[] { system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric() }, new CtorInfo(",", 5));
            var Tuple06Type = system.NewType("Tuple`6", new[] { system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric() }, new CtorInfo(",", 6));
            var Tuple07Type = system.NewType("Tuple`7", new[] { system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric() }, new CtorInfo(",", 7));
            var Tuple08Type = system.NewType("Tuple`8", new[] { system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric() }, new CtorInfo(",", 8));
            var Tuple09Type = system.NewType("Tuple`9", new[] { system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric() }, new CtorInfo(",", 9));
            var Tuple10Type = system.NewType("Tuple`10", new[] { system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric() }, new CtorInfo(",", 10));
            var Tuple11Type = system.NewType("Tuple`11", new[] { system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric() }, new CtorInfo(",", 11));
            var Tuple12Type = system.NewType("Tuple`12", new[] { system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric() }, new CtorInfo(",", 12));
            var Tuple13Type = system.NewType("Tuple`13", new[] { system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric() }, new CtorInfo(",", 13));
            var Tuple14Type = system.NewType("Tuple`14", new[] { system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric() }, new CtorInfo(",", 14));
            var Tuple15Type = system.NewType("Tuple`15", new[] { system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric(), system.NewGeneric() }, new CtorInfo(",", 15));

            // Populate the top level typing environment
            env["bool"] = env[@bool.Id] = @bool;
            env["int"] = env[@int.Id] = @int;
            env["string"] = env[@string.Id] = @string;
            env[SignatureType.Id] = SignatureType;
            env[ListType.Id] = ListType;
            new[]
            {
                Tuple00Type, Tuple01Type, Tuple02Type, Tuple03Type,
                Tuple04Type, Tuple05Type, Tuple06Type, Tuple07Type,
                Tuple08Type, Tuple09Type, Tuple10Type, Tuple11Type,
                Tuple12Type, Tuple13Type, Tuple14Type, Tuple15Type
            }.
            Aggregate(env, (e, t) => { e[t.Id] = t; return e; });

            // Bake some operator function types (to have something to infer about in familiar expressions)
            var binary1 = system.NewGeneric();
            var binary2 = system.NewGeneric();
            var binary3 = system.NewGeneric();
            var binary4 = system.NewGeneric();
            var binary5 = system.NewGeneric();
            var binary6 = system.NewGeneric();
            var binary7 = system.NewGeneric();
            var binary8 = system.NewGeneric();
            var binary9 = system.NewGeneric();
            var binary10 = system.NewGeneric();
            var binary11 = system.NewGeneric();

            // boolean operators ( bool -> bool ) and ( bool -> bool -> bool )
            // (e.g., "( ! ( empty ( 0 : ( ) ) ) )")
            system.Infer(env, Node.Define(Node.Var("!"), Node.Abstract(new[] { Node.Var("expr", @bool) }, @bool, Node.Const(@bool))));
            system.Infer(env, Node.Define(Node.Var("&&"), Node.Abstract(new[] { Node.Var("left", @bool), Node.Var("right", @bool) }, @bool, Node.Const(@bool))));
            system.Infer(env, Node.Define(Node.Var("||"), Node.Abstract(new[] { Node.Var("left", @bool), Node.Var("right", @bool) }, @bool, Node.Const(@bool))));

            // Polymorphic operator types
            system.Infer(env, Node.Define(Node.Var("+"), Node.Abstract(new[] { Node.Var("left", binary1), Node.Var("right", binary1) }, binary1, Node.Var("left"))));
            system.Infer(env, Node.Define(Node.Var("-"), Node.Abstract(new[] { Node.Var("left", binary2), Node.Var("right", binary2) }, binary2, Node.Var("left"))));
            system.Infer(env, Node.Define(Node.Var("*"), Node.Abstract(new[] { Node.Var("left", binary3), Node.Var("right", binary3) }, binary3, Node.Var("left"))));
            system.Infer(env, Node.Define(Node.Var("/"), Node.Abstract(new[] { Node.Var("left", binary4), Node.Var("right", binary4) }, binary4, Node.Var("left"))));
            system.Infer(env, Node.Define(Node.Var("%"), Node.Abstract(new[] { Node.Var("left", binary5), Node.Var("right", binary5) }, binary5, Node.Var("left"))));
            system.Infer(env, Node.Define(Node.Var(">"), Node.Abstract(new[] { Node.Var("left", binary6), Node.Var("right", binary6) }, @bool, Node.Const(@bool))));
            system.Infer(env, Node.Define(Node.Var(">="), Node.Abstract(new[] { Node.Var("left", binary7), Node.Var("right", binary7) }, @bool, Node.Const(@bool))));
            system.Infer(env, Node.Define(Node.Var("<"), Node.Abstract(new[] { Node.Var("left", binary8), Node.Var("right", binary8) }, @bool, Node.Const(@bool))));
            system.Infer(env, Node.Define(Node.Var("<="), Node.Abstract(new[] { Node.Var("left", binary9), Node.Var("right", binary9) }, @bool, Node.Const(@bool))));
            system.Infer(env, Node.Define(Node.Var("=="), Node.Abstract(new[] { Node.Var("left", binary10), Node.Var("right", binary10) }, @bool, Node.Const(@bool))));
            system.Infer(env, Node.Define(Node.Var("!="), Node.Abstract(new[] { Node.Var("left", binary11), Node.Var("right", binary11) }, @bool, Node.Const(@bool))));

            // A ternary if-then-else will come in handy too
            var ifThenElse = system.NewGeneric();
            system.Infer(env, Node.Define(Node.Var("if"), Node.Abstract(new[] { Node.Var("condition", @bool), Node.Var("then", ifThenElse), Node.Var("else", ifThenElse) }, ifThenElse, Node.Var("then"))));

            system.Infer(env, Node.Define(Node.Var("first"), Node.Abstract(new[] { Node.Var("pair", Tuple02Type) }, Tuple02Type[0], Node.Const(Tuple02Type[0]))));
            system.Infer(env, Node.Define(Node.Var("second"), Node.Abstract(new[] { Node.Var("pair", Tuple02Type) }, Tuple02Type[1], Node.Const(Tuple02Type[1]))));
            system.Infer(env, Node.Define(Node.Var("count"), Node.Abstract(new[] { Node.Var("list", ListType) }, @int, Node.Const(@int))));
            system.Infer(env, Node.Define(Node.Var("empty"), Node.Abstract(new[] { Node.Var("list", ListType) }, @bool, Node.Const(@bool))));
            system.Infer(env, Node.Define(Node.Var("head"), Node.Abstract(new[] { Node.Var("list", ListType) }, ListType[0], Node.Const(ListType[0]))));
            system.Infer(env, Node.Define(Node.Var("tail"), Node.Abstract(new[] { Node.Var("list", ListType) }, ListType, Node.Const(ListType))));
            system.Infer(env, Node.Define(Node.Var("length"), Node.Abstract(new[] { Node.Var("string", @string) }, @int, Node.Const(@int))));
            system.Infer(env, Node.Define(Node.Var("escape"), Node.Abstract(new[] { Node.Var("string", @string) }, @string, Node.Const(@string))));
            system.Infer(env, Node.Define(Node.Var("toString"), Node.Abstract(new[] { Node.Var("value", system.NewGeneric()) }, @string, Node.Const(@string))));
            system.Infer(env, Node.Define(Node.Var("parseInt"), Node.Abstract(new[] { Node.Var("string", @string) }, @int, Node.Const(@int))));

            // DRY helpers
            var isFunction = null as Func;
            isFunction = type => type != null ? (type.Constructor != null ? type.Constructor == TypeSystem.Function : isFunction(type.Self)) : false;
            Func @typeof = (id, arity) => id != null ? (new CtorInfo(id, arity).GetType(env) ?? (env.ContainsKey(id) && env[id].Value.Name.IsConstructor ? env[id].Value : null)) : null;
            Func isCtor = (id, arity) => @typeof(id, arity) != null;
            Func isArray = value => value is object[];
            Func array = value => (object[])value;
            Func isNil = value => isArray(value) && (array(value).Length == 0);

            // A sort of poor man's visitor (over the S-expr) : just a bunch of lambdas
            Func visitError = (scope, message) => { throw new InvalidOperationException(message); };
            Func visitSExpr = null;
            Func visitLet = null;
            Func visitDefine = null;
            Func visitApply = null;
            Func visitAbstract = null;
            Func visitCtor = null;
            Func visitVar = null;
            Func visitConst = null;
            Func visit;

            visitSExpr =
                (scope, sexpr, inType) =>
                {
                    var arity = (isArray(sexpr) ? array(sexpr).Length : 0) - 1;
                    var node =
                        isArray(sexpr) ?
                        (
                            // ( let / | / sexpr ... )
                            array(sexpr).Length > 1 ?
                            (
                                (Syntax.Identifier(array(sexpr)[0]) == null) || (Syntax.Identifier(array(sexpr)[0]) != "let") ?
                                (
                                    // (  / sexpr ... )
                                    Syntax.Identifier(array(sexpr)[1]) != "=>" ?
                                    (
                                        // ( sexpr ... )
                                        !isCtor(Syntax.Identifier(array(sexpr)[0]), arity) ?
                                        (
                                            !isCtor(Syntax.Identifier(array(sexpr)[1]), arity) ?
                                            // ( sexpr ... )
                                            visitApply(scope, sexpr, inType)
                                            :
                                            // ( sexpr  ... )
                                            visitCtor(scope, sexpr, 1, inType)
                                        )
                                        :
                                        // (  ... )
                                        visitCtor(scope, sexpr, 0, inType)
                                    )
                                    :
                                    // ( ... => ... )
                                    !inType ? visitAbstract(scope, sexpr) : visitError(scope, "'=>' not allowed in type annotation")
                                )
                                :
                                // ( let ... )
                                !inType ? visitLet(scope, sexpr) : visitError(scope, "'let' not allowed in type annotation")
                            )
                            :
                            (
                                // ( id / sexpr )
                                !isNil(sexpr) ?
                                (
                                    !isCtor(Syntax.Identifier(array(sexpr)[0]), 0) ?
                                    // ( sexpr )
                                    (Node)visitApply(scope, sexpr, inType)
                                    :
                                    // (  )
                                    visitCtor(scope, sexpr, 0, inType)
                                )
                                :
                                // ( )
                                visitConst(scope, ListType)
                            )
                        )
                        :
                        // id / const
                        Syntax.Identifier(sexpr) != null ? (Node)visitVar(scope, sexpr) : visitConst(scope, sexpr);
                    return node;
                };

            visitLet =
                (scope, sexpr) =>
                {
                    var let = Node.Let(array(array(sexpr)[1]).Select(item => visitDefine(scope, item, 0, false)).ToArray(), visitSExpr(scope, array(sexpr)[2], false));
                    return let;
                };

            visitDefine =
                (scope, sexpr, at, inType) =>
                {
                    var left = array(sexpr)[0];
                    Var identifier;
                    Node definition;
                    if (!inType && isArray(left) && (array(left).Length == 1))
                    {
                        var right = array(sexpr)[1];
                        var arity = (isArray(right) ? array(right).Length : 0) - 1;
                        identifier = visitVar(scope, array(left)[0]);
                        definition =
                            isArray(right) ?
                            (
                                array(right).Length > 1 ?
                                (
                                    !isCtor(Syntax.Identifier(array(right)[1]), arity) ?
                                    (
                                        !isCtor(Syntax.Identifier(array(right)[0]), arity) ?
                                        visitApply(scope, right, true)
                                        :
                                        visitCtor(scope, right, 0, true)
                                    )
                                    :
                                    visitCtor(scope, right, 1, true)
                                )
                                :
                                (
                                    !isNil(right) ?
                                    (
                                        !isCtor(Syntax.Identifier(array(right)[0]), 0) ?
                                        (Node)visitApply(scope, right, inType)
                                        :
                                        visitCtor(scope, right, 0, true)
                                    )
                                    :
                                    visitConst(scope, ListType)
                                )
                            )
                            :
                            Syntax.Identifier(right) != null ? (Node)visitVar(scope, right) : visitConst(scope, right);
                    }
                    else
                    {
                        identifier = visitVar(scope, array(sexpr)[at]);
                        definition = visitSExpr(scope, array(sexpr)[1 - at], inType);
                    }
                    var define = Node.Define(identifier, definition);
                    return define;
                };

            visitApply =
                (scope, sexpr, inType) =>
                {
                    Func newFunction = signature => system.NewType(TypeSystem.Function, signature);
                    Apply apply;
                    string id;
                    if (((id = Syntax.Identifier(array(sexpr)[0])) != null) && (!env.ContainsKey(id) || isFunction(env[id])))
                    {
                        var fn = Node.Var(id, !env.ContainsKey(id) ? env[id] = newFunction(array(sexpr).Skip(1).Select(arg => system.NewGeneric()).Concat(new[] { system.NewGeneric() }).ToArray()) : env[id]);
                        apply = Node.Apply(fn, array(sexpr).Skip(1).Select(arg => visitSExpr(scope, arg, false)).ToArray());
                    }
                    else
                    {
                        apply =
                            Node.Apply
                            (
                                visitSExpr(scope, array(sexpr)[0], inType),
                                array(sexpr).Skip(1).Select(arg => visitSExpr(scope, arg, inType)).ToArray(),
                                id != null ? env[id] : null,
                                inType
                            );
                    }
                    return apply;
                };

            visitAbstract =
                (scope, sexpr) =>
                {
                    Abstract lambda;
                    lambda =
                        Node.Abstract
                        (
                            array(array(sexpr)[0]).Select(arg => isArray(arg) ? (Node)visitDefine(scope, arg, 1, true) : visitVar(scope, arg)).ToArray(),
                            visitSExpr(scope, array(sexpr)[2], false)
                        );
                    return lambda;
                };

            visitCtor =
                (scope, sexpr, at, inType) =>
                {
                    var identifier = Syntax.Identifier(array(sexpr)[at]);
                    var isList = identifier == ((CtorInfo)ListType.Metadata).Cons;
                    var arity = at > 0 ? (array(sexpr).Length + 1) / 2 : array(sexpr).Length - 1;
                    var type = @typeof(identifier, arity);
                    var argv =
                        at > 0 ?
                        array(sexpr).Where((arg, i) => (i % 2) == 0).Select(arg => visitSExpr(scope, arg, inType)).Take(isList ? arity - 1 : arity).ToArray()
                        :
                        array(sexpr).Skip(1).Select(arg => visitSExpr(scope, arg, inType)).Take(isList ? arity - 1 : arity).ToArray();
                    var ctor = Node.Apply(Node.Var(type.Id), argv, isFunction(type) ? TypeSystem.Function : type, inType);
                    return ctor;
                };

            visitVar =
                (scope, sexpr) =>
                {
                    var var = Node.Var(Syntax.Identifier(sexpr));
                    return var;
                };

            visitConst =
                (scope, sexpr) =>
                {
                    var @const = Node.Const(sexpr);
                    return @const;
                };

            visit =
                (scope, sexpr) =>
                {
                    var root = visitSExpr(scope, sexpr, false);
                    return root;
                };

            Action analyze =
                root =>
                {
                    Func tryInfer =
                        node =>
                        {
                            try
                            {
                                return system.Infer(env, node);
                            }
                            catch (Exception ex)
                            {
                                return system.NewType(string.Format("Type error: {0}", ex.Message), null);
                            }
                        };
                    var sw = new System.Diagnostics.Stopwatch();
                    sw.Start();
                    foreach (var node in root.Args)
                    {
                        Console.WriteLine();
                        Console.WriteLine(node.Spec is Node ? string.Format("{0}:\r\n\t{1}", (Node)node.Spec, tryInfer(node).Value) : tryInfer(node).Value.ToString());
                    }
                    sw.Stop();
                    Console.WriteLine();
                    Console.WriteLine(string.Format("{0}:\r\n\t{1}", root.Body, tryInfer(root.Body)));
                    Console.WriteLine();
                    Console.WriteLine("... Done (in {0} ms)", sw.ElapsedMilliseconds);
                    Console.WriteLine();
                };

            // Parse some S-expr's from string representation
            // (single-line comments start with "//" and end on their line)
            var parsed =
                syntax.
                Parse
                (@"
                    ( let
                        (
                            ( id ( ( x ) => x ) )

                            ( factorial ( ( n ) => ( if ( > n 0 ) ( * n ( factorial ( - n 1 ) ) ) 1 ) ) )

                            ( f_o_g ( ( f g ) => ( ( x ) => ( f ( g x ) ) ) ) )

                            // See http://lambda-the-ultimate.org/node/5408
                            ( f ( ( x ) => ( ( g true ) , x ) ) )                 // ML-ish: f x = (g True, x)

                            ( g ( ( b ) =>
                                ( if b
                                    0                                             // ML-ish: g True = 0
                                    ( + ( first ( f ""a"" ) ) ( first ( f 0 ) ) ) // ML-ish: g False = fst (f 'a') + fst (f 0)
                                )
                            ) )

                            // See (page 3)
                            // [Fritz Henglein] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.388.430&rep=rep1&type=pdf

                            ( fmap (
                                ( f l ) =>
                                ( if ( ! ( empty l ) )
                                    ( ( f ( head l ) ) : ( fmap f ( tail l ) ) )
                                    ( )
                                )
                            ) )

                            // See (page 3, examples ""Double"", ""Mycroft"", ""Sum List"", ""Composition""...)
                            // [Hallett & Kfoury] http://itrs04.di.unito.it/papers/hk.pdf

                            // Double
                            ( double ( ( f ) => ( ( x ) => ( f ( f x ) ) ) ) )
                            ( foo ( ( n ) => ( ( double ( ( num ) => ( + num 1 ) ) ) n ) ) )
                            ( bar ( ( s ) => ( ( double escape ) s ) ) )

                            // Mycroft
                            ( sqList ( ( l ) => ( fmap ( ( x ) => ( * ( + x 0 ) x ) ) l ) ) )
                            ( compList ( ( l ) => ( fmap ! l ) ) )

                            // Sum List
                            ( sumList ( ( l ) =>
                                ( if ( empty l )
                                    0
                                    ( + ( id ( head l ) ) ( sumList ( id ( tail l ) ) ) )
                                )
                            ) )

                            // Isomorphic Compositions
                            ( createList ( ( x ) => ( x : ( ) ) ) )
                            ( removeList ( ( l ) => ( head l ) ) )
                            ( comp ( ( f g ) => ( f_o_g f g ) ) )
                            ( appComp ( ( v1 v2 ) =>
                                ( ==
                                    ( ( comp removeList createList ) v1 )
                                    ( head ( ( comp createList removeList ) v2 ) )
                                )
                            ) )

                            ( threeValuesToAListOfTriples (
                                ( a b c ) => ( ( a , b , c ) : ( ) )
                            ) )
                            ( twoValuesToAPairOfLists (
                                ( a b ) => ( ( a : ( ) ) , ( b : ( ) ) )
                            ) )

                            // demonstrates type annotations
                            ( ( Pair ) ( a -> b -> ( ( a , b ) this ) ) ) // ( Pair a b ) just an alias for ( Tuple`2 a b )
                            
                            ( ( Atoi ) ( string -> int ) ) // string to integer converter signature

                            // should be inferred as,
                            // atoiTest : ( string -> int ) -> ( List string ) -> ( List ( string , int ) )
                            ( atoiTest (
                                (
                                    ( Atoi convert ) // (the converter)
                                    l // (some list)
                                )
                                => ( ( ( head l ) , ( convert ( head l ) ) ) : ( atoiTest convert ( tail l ) ) )
                            ) )

                            ( ( Triples ) ( x -> y -> z -> ( ( ( ( x , y , z ) triple ) : ( ) ) this ) ) )
                            ( Cloud ( ( v ) => ( Triples v v v ) ) )
                            ( number-cloud ( Cloud 0 ) )
                            ( string-cloud ( Cloud """" ) )

                            // advanced / more interesting:
                            // demonstrates generic type annotations
                            // mixed with constructor syntax ...
                            ( moreInteresting (
                                (
                                    // (`f' takes an `a' and returns a pair of `a' and `b')
                                    ( ( a -> ( ( a , b ) p ) ) f )
                                    l
                                ) =>
                                // `l' will be inferred to inhabit `( List a )' ...
                                // ... and as for the result of moreInteresting,
                                // to inhabit `( List b )'
                                ( ( second ( f ( head l ) ) ) : ( ) )
                            ) )

                            ( testOutput1 ( threeValuesToAListOfTriples 1 ""a"" true ) )
                            ( testOutput2 ( twoValuesToAPairOfLists 1 ""a"" ) )                            

                            // moreInteresting which will typecheck
                            ( testOutput3 (
                                moreInteresting
                                ( ( s ) => ( s , ( parseInt s ) ) ) // ... that's for the formal `f' (a lambda)
                                ( ""1"" : ( ""2"" : ( ) ) ) // ... that's for the formal `l'
                            ) )
                            // moreInteresting which cannot typecheck
                            ( testOutput3CannotTypecheck (
                                moreInteresting
                                ( ( s ) => ( s , ( parseInt s ) ) )
                                ( 1 : ( 2 : ( ) ) )
                            ) )
                        )

                        // report type inference results thru a fat tuple in let's body
                        //( uncomment whatever you're interested in )
                        (
                            ( id ( 0 , ""1"", true ) )
                            //, ( fmap ( f_o_g factorial parseInt ) ( ""0"" : ( ""1"" : ( ""2"" : ( ""3"" : ( ) ) ) ) ) )
                            //, ( first ( f true ) )
                            //, ( foo 123 )
                            //, ( bar ""z"" )
                            //, ( sqList ( 0 : ( 1 : ( 2 : ( 3 : ( ) ) ) ) ) )
                            //, ( compList ( true : ( false : ( ) ) ) )
                            //, ( sumList ( 1 : ( 2 : ( 3 : ( ) ) ) ) )
                            //, ( appComp 5 ( 5 : ( ) ) )
                            , testOutput1
                            , testOutput2
                            , testOutput3
                            , testOutput3CannotTypecheck
                        )
                    )
                ");

            var ast = visit(env, parsed);

            Console.WriteLine();
            Console.WriteLine("Abstract syntax:");
            foreach (var node in ast.Args)
            {
                Console.WriteLine();
                Console.WriteLine(node);
            }

            Console.WriteLine();
            Console.WriteLine("Inferred types:");

            // Visit the parsed S-expr, turn it into an AST for H-M type inference
            // (see Node, et al, above), infer some types from the latter,
            // and report
            analyze(ast);
        }
    }
}