Programming contest: Type checker.

Task: Write a type checker and inference engine for this small statically typed language (parser and evaluator optional. You may enter the AST directly in the source code, and you only need to ensure that invalid programs are failed and valid ones are passed).


; def: (def symbol arguments code), (def symbol code) or (def symbol)
; ∀: (∀ (variables) ((constraints)) code) returns code
; ∷: (∷ symbol type) returns symbol, type-annotated.
; →: (→ type1 type2 … returnType) returns type
; #+: primitive + of type (→ Int Int Int)

(def (∷ + (→ Int Int)) (x) x)
(def (∀ (χ) ((∷ + (→ Int . χ))) (∷ + (→ Int Int . χ)))
    (x y . r) (+ (#+ x y) . r)))

; (+ 1 1 1) → 3
; (+ 1 1 1 1) → 4
; ((+ 1) 1) → 2 (the language is curried)

; Interface example, assume an IO monad, String, write and sprintf:
(def (∷ Writeable (∀ (χ) ((∷ write (→ χ String (IO ())))) χ)))
(def (∷ fprintf (∀ (χ α) ((∷ Writeable χ) (∷ sprintf (→ ,@α String))) (→ χ ,@α (IO ()))))
    (a . b) (write a (sprintf . b))
Everything type annotation except the interface example should be able to be inferred. Feel free to improve the syntax of types that now use unquote-splicing as long as the semantics are the same.

The winner will be decided on the 1st of January. Criterions will be code size, elegance, helpfulness of error messages, and speed.

2011
using sexp syntax instead of mlite for typed lambda calculi

laughingirls.jpg

oh fuck no, the hellish type system of haskell combined with the readability of lisp

what a fucking miserable attempt at describing a type system.

>>2
mlite?

why is there math near my /g/

>>2
If you mean something like ML, then it's partly because SEXP has an easier AST for the purposes of this contest. Also, I think it will be a lot sexier with SRFI 49 and without type annotations.

>>4
Was there something you failed to understand?

the fuck am i looking at

>>7
SEXP has an easier AST

SEXP has an easier AST

SEXP has an easier AST

What


the


fuck


am


I










reading


???


Are you seriously this stupid? really???

>>7
you haven't explained the type rules, you just gave the (horrible horrible) syntax and a couple examples

nominated for /prog/ worst thread of 2011

(def (∷ Writeable (∀ (χ) ((∷ write (→ χ String (IO ())))) χ)))
(def (∷ Writeable (∀ (χ)
(def (∷ Writeable (∀
Writeable (∀
(∀

(ﾟ∀ﾟ)

>>10
What exactly isn't obvious? There's ad-hoc polymorphism, types are the same types as in System F, (∀ (α) ((constraints)) …) means every type α matching the constraints, the … can be replaced by any code and denotes the scope of those type variables, a constraint (∷ x <type containing variable(s)>)) means that the type variable in the ∀ is constrained to only types matching the type signatures of that symbol, how (→ Int . χ) and (→ χ ,@α String) constrains the variables should be plainly obvious, etc. etc. It's serioulsy straight forward, and if I've fucked up and there's an ambiguity, just ask.

>>9
Yeah, whatever, so SEXP is really a serialization of the AST of the underlying language, whatever. Does it matter for the contest at hand? Thought not.

>>9-11
Go back to /lounge/ or /b/

>>14
( ° ∀° )

[parentheses [give [me [a [huge [autistic [boneresque [boner 'powered-by-bbcode]]]]]]]]

Somebody translate this into something I can understand, like Bonerlang

>>13
lol mad and stupid


#include <boner.h>

boner boner(boner boner, boner* boner[])
{
    boner(boner, "Boner\n");
    boner boner;
}

use döner;

döner
    döner = döner;

döner
    döner("döner");
    döner döner;
döner;

bonerlang's type system is weak without BONADS


polecat kebabs polecat kebabs(polecat kebabs polecat kebabs)
    polecat kebabs << "polecat kebabs" << polecat kebabs;
polecat kebabs;

#polecat kebabs "polecat kebabs"
polecat kebabs(polecat kebabs polecat kebabs)
{
   polecat kebabs(polecat kebabs << polecat kebabs);
   polecat kebabs;
}

Time is running out!

It looks awful, I will not give life to this thing.

static typing
Thanks but I write programs to solve novel problems not reimplement the solutions of others.

Here you have:

(let ((validate-code (lambda () (display "Invalid code!")
                                (newline)
                                (exit 1))))
  (validate-code))

>>21
It should actually be that Bonerlang makes use of [b][i][o][u]GONADS[/u/][/o][/i][/b]