I'm just wondering what you guys think of this syntax. How much can you decipher without any explanation? I posted this to 4chan's /prog/, but they were too busy achieving satori.
[code]
# This is a comment.
Nat : Type;
0 : Nat;
succ : Nat > Nat;
#!
!#
List : Nat > Type > Type;
nil : t < List 0 t;
cons : n < t < t > List n t > List (succ n) t;
sum : n < List n Nat > Nat
= $cons x xs? + x (sum xs)
| $nil! 0;map : n < a < (a > a) > List n a > List n a
= f! $nil? nil
| $cons x xs! cons (f x) (map f xs);(foldr : n < a < b < (a > b > b) > b > List n a > b)
f z = $nil? z
| $cons x xs! f x (foldr f z xs);(foldr1 : n < a < b < (a > b > b) > b > List (succ n) a > b)
f z ($cons x xs) = foldr f x xs;foldl f z = $nil? z
| $cons x xs! foldl f (f z x) xs;foldl1 f ($cons x xs) = foldl f x xs
Matrix : Nat > Nat > Type > Type
mkMatrix = m < n < t < List m (List n t)
mul : a < b < c < t < Matrix a b t > Matrix b c t > Matrix a c t
= #not implemented yet.[/code]
Something tells me the formatting of that code is screwed up, try again after disabling WakabaMark.
Whoops.
`
# This is a comment.
Nat : Type;
0 : Nat;
succ : Nat > Nat;
#!
!#
List : Nat > Type > Type;
nil : t < List 0 t;
cons : n < t < t > List n t > List (succ n) t;
sum : n < List n Nat > Nat
= $cons x xs? + x (sum xs)
| $nil! 0;map : n < a < (a > a) > List n a > List n a
= f! $nil? nil
| $cons x xs! cons (f x) (map f xs);(foldr : n < a < b < (a > b > b) > b > List n a > b)
f z = $nil? z
| $cons x xs! f x (foldr f z xs);(foldr1 : n < a < b < (a > b > b) > b > List (succ n) a > b)
f z ($cons x xs) = foldr f x xs;foldl f z = $nil? z
| $cons x xs! foldl f (f z x) xs;foldl1 f ($cons x xs) = foldl f x xs
Matrix : Nat > Nat > Type > Type
mkMatrix = m < n < t < List m (List n t)
mul : a < b < c < t < Matrix a b t > Matrix b c t > Matrix a c t
= #not implemented.`
What the hell? Every line? Really?
>>4
Just load your code in some buffer, and M-S-< C-x ( M-4 <space> C-x ) M-1000 C-x e
I must be some sort of idiot. Here comes the third try:
<code>
# This is a comment.
Nat : Type;
0 : Nat;
succ : Nat > Nat;
#!
+ : Nat > Nat > Nat
= $0? m! m
| $succ n? m! + n (succ m);
!#
+ m = $0? m
| $succ n! + (succ m) n;
List : Nat > Type > Type;
nil : t < List 0 t;
cons : n < t < t > List n t > List (succ n) t;
sum : n < List n Nat > Nat
= $cons x xs? + x (sum xs)
| $nil! 0;
map : n < a < (a > a) > List n a > List n a
= f! $nil? nil
| $cons x xs! cons (f x) (map f xs);
(foldr : n < a < b < (a > b > b) > b > List n a > b)
f z = $nil? z
| $cons x xs! f x (foldr f z xs);
(foldr1 : n < a < b < (a > b > b) > b > List (succ n) a > b)
f z ($cons x xs) = foldr f x xs;
foldl f z = $nil? z
| $cons x xs! foldl f (f z x) xs;
foldl1 f ($cons x xs) = foldl f x xs
Matrix : Nat > Nat > Type > Type
mkMatrix = m < n < t < List m (List n t)
mul : a < b < c < t < Matrix a b t > Matrix b c t > Matrix a c t
= #not implemented.</code>
the <code> tags aren't even necessary, are they?
>>6
lurk more
or simply RTFM
What's up with functional programmers and non-descriptive variable names? Fuck you guys. Learn how to write readable and maintainable code.
I'm a huge fan of referential transparency, I just hate the culture that has grown up around it.
Alas, I haven't read my TAPL, nor am I fan of Haskell or Agda. Having said that, I think I understood it till this point:
cons : n < t < t > List n t > List (succ n) t;Okay, you're consing, but I don't understand what's going on with those <, and I concur with >>9's sentiment.
Also, I am not a fan of currying. It seems so clever until you realize how limited it is: one arg at a time, left to right. And then it fags > up > all > your > type > signatures. Bah.
What I understood from that sample is that
#! ... !#is a multi-line comment,
n <basically means foreach n or specifies that n is inferred,
$ ? !are somehow used for pattern matching but I can't seem to figure out exactly how. I also can't figure out what f! does.
You also got
mkMatrix = m < n < t < List m (List n t)and
foldr1 : n < a < b < (a > b > b) > b > List (succ n) a > bwrong.
lame