03:37:50 <pikhq> I even grant you the usage of the "0.0.0" portion of Dimensifuck syntax, since that's not Brainfuck-based at all. ;)

03:38:28 <ihope> (Actually, they're The Natural Way, since most natural languages I've seen are declarative.)

03:45:47 <ihope> You can grab an older version of Python and present it to... um, the functional people.

03:53:14 <ihope> Put a ball in 1, get a ball out A. Put a ball in 2, get a ball out B if there was a ball in 1 or C if there wasn't.

03:54:25 <ihope> If you have an infinite pool table with an infinite number of obstacles, it's Turing-complete.

04:01:47 <ihope> But given that this is all about building tiny, energy-efficient computers, don't expect them to work :-P

04:29:58 <oklopol> www.vjn.fi/gz/onokki.exe eve though i'm pretty sure no one is gonna open these :P

04:35:24 <oklopol> (btw in case you try onokki, i can move to anywhere on the screen in ~ 6 seconds)

04:49:58 <oklopol> that was the link to the dll, by the way, don't know if you just thought it was another gamme

04:51:46 <oklopol> i wish i still got great ideas like making a game that's controlled with one button

05:07:56 <oklopol> even though there is just one button, there are actually two kinds of manouvering

05:08:56 <oerjan> well i did manage to get stuck in a corner for a while, still haven't broken the code

05:13:14 <oklopol> the beauty of having just one button per player is that 7 players can use the same kayboard

07:53:28 <edwardk> are the esoteric languages in question here esoteric as in hard to use/pointless brainf*ck kind of things or esoteric as in non-mainstream, unusual and interesting?

07:55:23 <edwardk> been working on a toy interpreter/compiler for a lazy programming language with first class subset/quotient types and looking for a place to talk to people about it, that fit the general gamut of this place?

08:00:23 <edwardk> basically what i have right now is an interpreter written in haskell for this thing, and a compiler i've been slowly working on bootstrapping in it. the language is sort of a kitchen-sink repository of anything cool-but-undecidable-in-general in type theory circles.

08:01:10 <pikhq> Just with the word "haskell", you've gotten Oerjan's approval (although he's not here ATM)

08:01:21 <edwardk> hopefully in a couple months i should have something stable enough to start being useful

08:02:58 <edwardk> bsmntbombdood: : the idea is that you can define a subset type of an existing type by stating a predicate using the syntax of the base language for the predicate. so example Nat = { x : Int | x >= 0 } would be a subset type taken from the Ints

08:03:13 <pikhq> (although I'm thinking about making Brainfuck knowledge mandatory for the channel. :p)

08:03:29 <edwardk> or if i have sorted : Ord a => [a] -> Bool as a predicate written in the base language

08:04:07 <edwardk> using a subset type on the result to specify that the result will satisfy the in-language predicate above

08:04:13 <pikhq> edwardk: Hmm. I like, so far. . . Not sure I'll be able to wrap my head around all of it, though. :p

08:05:02 <edwardk> f : { x : T1 | pre x } -> { y : T2 | post x y } defines a compile-time-checked contract of the pre and post conditions on f

08:05:38 <edwardk> so if i can prove it you hear nothing from the compiler, if i can concretely disprove it with a counter example you get an error and the counter example, shrunk haskell quickcheck style

08:05:58 <edwardk> if i can't prove it you get a warning and an option to insert a runtime check for the condition, since the predicate is written in the base language

08:06:15 * pikhq goes to the comfort of a Brainfuck interpreter. Could someone that's actually taken computer science make edwardk feel welcome, instead? :p

08:07:50 <edwardk> anyways thats one undecidable-but-cool feature, and its probably the most useful one that I have been working towards

08:08:45 <edwardk> yeah, like i said, type checking the above tries to prove it, if it can, and if it can't, it falls back on inserting a runtime check

08:08:58 <edwardk> so a lot of things like array bounds checking can be caught that way at compile time

08:09:24 <edwardk> quotient types are a little harder to motivate and unfortunately lack the runtime fall-back.

08:11:10 <edwardk> subset types let you define an arbitrary subtype for any type in the language by using predicates defined in the language. quotient types let you go the other way and let you define arbitrary supertypes for types in the language by redefining equality on them and incurring a proof burden every time you use them in argument-position to a function that is defined over the base type.

08:12:35 <edwardk> and if you ask of 4 == even, it'll say yes because 4 :: Parity == 0 :: Parity since 4 mod 2 == 0 mod 2

08:15:54 <edwardk> anyways syntax-like its kind of like haskell, with the addition that you use the same function syntax at the type and term levels -- giving it somewhat less syntax to learn there, but blowing the syntax budget on polymorphic records, etc.

08:25:49 <edwardk> anyways it probably doesn't qualify as esoteric, simply because its designed to be useful ;)

08:30:57 <pikhq> edwardk: It's an interesting concept for a programming language. I'd say it fits with the populace here if not the topic. ;)

08:31:39 <pikhq> BTW, some of the oddest esoteric languages have been designed with some sort of usefulness in mind. . .

08:32:00 <edwardk> basically my goal right now is to get the compiler bootstrapped and generate some decent code from it

08:32:49 <pikhq> (I believe one was designed to disprove the strong claim of the wire crossing problem

08:35:18 <pikhq> Another esolang was designed with the idea of making it trivial to design cellular automatons.

19:09:46 <ihope> If there's a continuous bijection between RxR and RxR that maps S onto T, then S and T are equivalent.

19:12:51 <ihope> And... egad, there's so much stuff that's so easy to grasp intuitively yet so hard to express formally...

19:15:23 <ihope> The idea I'm wanting to capture is that of what could easily be written by a pen such that a little bit of sloppiness doesn't matter.

19:16:02 <ihope> Something like the letter O would be invalid because the starting and ending points would have to match perfectly.

19:16:36 <ihope> Same for the letter T: the one end of the vertical line has to go exactly as far as the horizontal line.

19:50:09 <ihope> Well, we'll say that a statement has to be a union of finite curves with endpoints such that the only "special points" are where a curve goes through a curve.

19:53:11 <ihope> A statement has to be a union of finite curves with endpoints such that all singular points are stable!

21:14:52 <ihope> + is an intersection, | is a straight line, - is a straight line... I guess some creativity is needed for corners.

21:38:15 <edwardk> For a second there I thought the curves involved were real curves, like NURBS or something. hrmm there is an esoteric language for you

21:39:44 <edwardk> well, i was a computational geometer for a while, i'm pretty comfortable with NURBS ;)

21:41:01 <edwardk> now, try to explain to the end user what a sequence of knots and weights is supposed to do

21:42:30 <edwardk> its not a language, just a way to specify curves in a projectionally invariant manner

21:47:35 <oklopol> innumerable brainfuck: a function and a range a...b is specified, then for every result of that function in that range is given it's own thread (infinite threads that is), so that every thread has a real number representing an infinite number of brainfuck instructions to execute (base 8 presentation); should a thread be given a faulty bf program it dies; the memory is shared, and it's continuous, > will move one derivative and has to be executed infinit

21:49:12 <edwardk> ihope: if you use a perspective projection on a bezier curve then subdivide it you get a different curve than if you subdivide it and then project it. NURBS provide the non-uniform subdivision necessary to be able to project something into 'viewspace' and get the same curve cutting it up there as before. it means its more useful for computer graphics applications

21:49:43 <oklopol> of course, running innumerable threads would be impossible even if we were given an infinite space to use for the computer :)

21:52:49 <oklopol> i mean, you can write a program in it that can predict any superturing program's result.

21:54:00 <ihope> What do you call one that can just solve the halting problem of a super-Turing program?

21:55:27 <ihope> (So a super^2-Turing program can solve the halting problem for super-Turing programs where a super-Turing program can solve the halting problem for a Turing program?)

21:56:47 <ihope> What if we say that a rank-0 machine is a Turing machine, and a rank-n machine is one that can solve the halting problem for rank_m machines for all m < n?

21:57:17 <edwardk> iirc grigori rosu used it when describing the complexity of proving the equivalence of two infinite streams last year at the ICFP but its an older notation

21:57:53 <ihope> Gets problematic when you get to an ordinal number n that can't be described by a rank-(n+1) machine.

21:58:45 <edwardk> http://fsl.cs.uiuc.edu/index.php/Equality_of_Streams_is_a_Pi_2%5E0-Complete_Problem

22:00:34 <ihope> ...here are two properties of ordinal numbers: for every set of ordinal numbers, there's a lowest ordinal number bigger than all those in the set; and for every ordinal number, there's a set containing exactly those ordinal numbers below that ordinal number.

22:02:54 <oklopol> to me, that's a tautology, but you've prolly read a lot more about infinities than me

22:05:05 <edwardk> http://www.mtnmath.com/whatrh/node51.html introduces Pi_2 mentioned above, and goes on to ordinals from there

22:06:32 <ihope> If a set is order isomorphic to a set of ordinal numbers containing exactly those ordinal numbers below n, then n is said to be the order type of that set.

22:07:22 <edwardk> http://ecommons.library.cornell.edu/bitstream/1813/6877/1/89-961.pdf also talks about it

22:21:40 <edwardk> My toy project has been all about 'nibbling at the edges' of undecidability there.

22:36:27 <edwardk> wandered in here last night trying to find a place where talking about a language-in-progress wouldn't put everyone to sleep ;)

22:41:10 <edwardk> the reaction from last night went: (3:00:47 AM) pikhq: Just with the word "haskell", you've gotten Oerjan's approval (although he's not here ATM)

22:45:23 <edwardk> what i have is basically a haskell-like syntax, from the standpoint of minimal keywords and you just say foo x y = .. to define a function, and give it a haskell like type signature

22:45:40 <edwardk> except for the fact that type level functions use the same syntax as term level ones

22:46:32 <edwardk> and that i have subset and quotient types for contract checking and polymorphic records and variants, to give you a reasonable OOP and extensible version of 'data' declarations, ala ocaml

22:48:09 <edwardk> but i noted that i can leverage the same syntax i use for field dereferencing for named arguments

22:49:18 <edwardk> dependent types can only affect predicates, therefore they have limited runtime effect

22:49:50 <edwardk> though i have type families so thats not entirely true, there are other cases of dependent types, but basically they all resolve with phase distinction

22:51:19 <edwardk> say, we want to prove the correctness of a sort routine, but we don't want to go off and write it in coq

22:52:24 <oerjan> undecidability in theory is one thing, but the real question is whether the type inference can terminate on practical examples

22:52:52 <edwardk> in my case though you can make it so you can explicitly pass in the order there. sorted (.by : Ord a) => [a] -> Bool gives you the ability to explicitly pass the dictionary

22:53:52 <oerjan> heh i noticed automatically greating *By functions was mentioned on #haskell before i gave up

22:54:02 <edwardk> so, going with the sorted example you can build it up like haskell sorted [] = True; sorted [x] = True; sorted (x:xs) = x <head xs && sorted xs

22:55:33 <edwardk> where ( x : T | P x) is a predicate subtype, like mathematicians write { x : T | P x }, i just need { }'s for records so i swap unambiguously to ()'s

22:56:49 <edwardk> specifies pre conditions necessary to call the function and post conditions of what it gaurantees

22:57:24 <edwardk> a quotient type is where you redefine equivalence over the type, in this case it interacts in somewhat interesting ways with the rest of the type system

22:58:59 <edwardk> anyways, we can define the sort above, sort [] = []; sort (x:xs) = insert x (sort xs) where insert : a -> (xs : [a] | sorted xs) -> (ys : [a] | sorted ys) has the obvious definition

23:00:34 <edwardk> and if you don't want to limit the use of insert you can go to a more liberal definition: insert : Ord a => a -> (xs : [a]) -> (ys : [a] | sorted xs ==> sorted ys) --- er i forgot the Ord a => constraint in the insert above

23:01:13 <edwardk> anyways the compiler just uses a form of abstract interpretation and the octagon abstraction domain for integer operations

23:01:58 <edwardk> if it can't prove the correctness of the output or input it insert a runtime check and warns, if it can provide a counter example at compile time it gives you that and a trace

23:02:39 <oklopol> oerjan: there is also a small quirk there, you see gravity is not 2d, but separate for both axes :)

23:04:14 <bsmntbombdood> * oklopol wishes he'd understand enough of that to be able to say something

23:05:01 <oklopol> don't try to crack that, oerjan :D it should go towards the light spots, but it's just a quick add and doesn't work that well

23:06:44 <oklopol> i think it find the lightest pixel around the ball on 32 pixel range and goes towards it

23:07:12 <oklopol> i have no idea whether i have a virus scan, i've never really believed in viruses :)

23:07:19 <edwardk> ihope: well, its not exactly an obscure feature, adding compile-time-checked contracts in the same language the end-user is already familiar with writing their code in strikes me as rather front-and-center from a usable powerful feature standpoint =)

23:07:32 <oerjan> it is hard to crack because unless you manage to get away from the swarm all the effects are so small

23:09:04 <edwardk> bstmtb: you can do so only with + and only if the inferred type of the n+k pattern is a member of the Integral typeclass

23:09:25 <oerjan> bsmntbombdood: the x+n pattern is about the only thing which is a multiargument function

23:09:38 <edwardk> oerjan: not really because i break everything else in the language on the way to get usable records and my type syntax looks nothing like it beyond the trivial examples

23:09:51 <edwardk> oerjan: but haskell is the easiest launching off point for me to take when explaining it

23:11:27 <edwardk> also, you can give classes names which dramatically changes the semantics of passing them, since an instance is just a dependently typed record you guarantee to exist

23:11:58 <oklopol> oklotalk can invert functions, -Func will do it... unfortunately that's one of the superturing things that will most like just crash :)

23:12:08 <edwardk> that way you can HAVE multiple instances of Ord for Int, one default, a bunch named, and you can pass in the named one to sort using that sort .by foo syntax

23:12:33 <edwardk> first class extensible records with subtyping also mucks with a lot of the haskell properties

23:13:40 <edwardk> oerjan: you can refer to their members by the name you gave the dictionary inside the function if the typing is ambiguous otherwise if there is only one way to unify it'll choose the right one

23:15:09 <edwardk> so in the above with sorted : (.by : Ord a) => [a] -> Bool; sort (x:xs) = x <=_by head xs && sorted xs exploits the fact that i allow foo.bar and bar_foo to be used as synonyms so that you can to infixed operators looked up in records.

23:17:09 <edwardk> dictionary passing is a bit more complicated by the fact that i want to pass a single polymorphic dictionary record when possible, so multiparameter type classes incur some weirdness

23:19:21 <oklopol> the idea why i'm making stuff like that in oklotalk is to make them work with simple math expressions

23:19:22 <ihope> Doing it quickly means you can construct a function proof -> sentence and invert it to prove any provable sentence :-)

23:22:18 <oerjan> ihope: as far as i know quantum computing is not known to be sufficient to invert all functions quickly, as in there is no quantum algorithm to solve NP-complete problems in polynomial time

23:23:16 <ihope> Inverting gets weirder when you bring foralls in: forall a. a -> * = (exists a. a) -> * whose inverse is * -> exists a. a

23:27:19 <oklopol> actually, i'm pretty sure read there isn't one, and that was less than a year ago

23:27:50 <oerjan> oklopol: there is an algorithm for checking if a number is a prime in polynomial time

23:27:53 <bsmntbombdood> if prime checking was the same as factoring most public key cryptographic algorithms would be pointless

23:28:51 <oklopol> bsmntbombdood: i mean it's the same if you just care about p/np and assume it needs to be deterministic

23:29:26 <oklopol> oerjan: i might recall wrong, my memory likes to carefully change all the new facts to what i assumed myself

23:34:55 <oerjan> in the (mod n, x^r-1) case it means that you first take the remainder of a polynomial division by x^r-1, then you mod all coefficients of the result by n

23:38:54 <oerjan> first you divide x^3 + 5 by x^2 + 1, now x^3 + 5 = x*(x^2 + 1) - x + 5, so the remainder is - x + 5

23:42:46 <oerjan> there is not always agreement on that: Haskell has mod and rem that behave differently with negative numbers

23:47:35 <oerjan> to be a little more precise, since there might be some choices of m and n where my approach subtly fails:

23:48:26 <oerjan> a == b (mod m, n) means that a-b = m*x + n*y, where x and y are elements of the ring (in the article case, polynomials with integer coefficients)

23:49:19 <ihope> You know, a language based on the topologies of things like http://pastebin.ca/607871 actually would be a little insane.

23:53:14 <oerjan> the first approach reduces an expression to a simpler one (mod m, n), this is sound but if we were dealing with two polynomials rather than one number and one polynomial as in the article, then you might not necessarily reach a unique form just by doing it in sequence

23:54:15 <oerjan> as in, it might be possible to continue dividing by m and n alternately without immediately reaching the same result

23:55:11 <oklopol> oerjan: i understand how you do that, but i can't really figure out what it actually means :P

23:57:02 <oerjan> oklopol: it is all about quotient rings. You get the ring of integers mod n by identifying every two integers that have the same remainder mod n