00:22:50 -!- oerjan has quit ("Habemus panem tostum?").
00:22:58 -!- timotiis has quit (Read error: 110 (Connection timed out)).
00:27:50 -!- olsner has quit ("Leaving").
00:32:22 <ehird> psygnisfive: Sorry. I'm such a faggotfag.
00:38:04 -!- BMeph has quit (Read error: 104 (Connection reset by peer)).
01:10:26 -!- sebbu has quit ("@").
01:20:09 -!- Core-un has joined.
01:31:12 <ehird> Core-un: Compiled haskell?...
01:32:14 <ehird> psygnisfive: Shut up, you.
01:32:48 <psygnisfive> you'll have to stick your cock in my mouth to make that happen
01:33:10 <ehird> psygnisfive: uh, thanks, but shut up
01:34:07 <ehird> Core-un: are you a reference to ghc/yhc core? :P
01:34:25 <Core-un> Just people were pronouncing my nick wrong
01:34:32 -!- Core-un has changed nick to Corun.
01:34:38 <ehird> Corun: oh then your nick sucks
01:35:45 <lament> what's with all the gay sex
01:35:53 <ehird> lament: you want to know do you?
01:36:02 <lament> it's like this channel is turning into #linguistics
01:38:54 -!- Polar has joined.
01:40:47 <ihope> We have a #linguistics?
01:43:28 -!- AAAAAAue4njxuz has quit (Read error: 104 (Connection reset by peer)).
01:43:33 -!- AAAAAAue4njxuz has joined.
01:43:37 -!- ehird has quit (Remote closed the connection).
01:44:00 -!- AAAAAAue4njxuz has changed nick to Quendus.
01:47:01 -!- boily has joined.
01:54:29 <lament> i shouldn't have mentioned #linguistics, now all the gay sex moved there instead
01:55:01 <ihope> I didn't know speaking Spanish was a form of gay sex.
01:58:24 -!- Corun has quit ("This computer has gone to sleep").
02:33:26 -!- Quendus has changed nick to AAAAAAue4njxuz.
02:38:18 -!- ihope has quit ("ChatZilla 0.9.82.1 [Firefox 2.0.0.14/2008040413]").
02:52:10 -!- boily has quit ("Leaving.").
03:48:55 -!- Polar has quit (leguin.freenode.net irc.freenode.net).
03:48:57 -!- cmeme has quit (leguin.freenode.net irc.freenode.net).
03:57:24 -!- Polar has joined.
03:57:24 -!- cmeme has joined.
04:01:04 -!- Sgeo has quit (Connection timed out).
04:33:36 <Deformative> I am trying to prove that a language is turing equivalent, how would I do this? Is implementing a turing machine an acceptable proof? What other tests are there?
05:30:57 <lament> more specifically, implementing a compiler from a turing-complete language to your language.
05:31:14 <lament> there's a bunch of nice turing-complete languages for which it is easy to write a compiler
05:31:33 <lament> LSK combinatory logic is another
05:32:04 <lament> register machines are another
05:35:09 <lament> (note that the compiler itself can be written in anything)
05:35:45 <lament> or writing an interpreter for that language in your language.
05:57:26 <psygnisfive> implementing a turing machine should be relatively simple to do tho
05:57:55 <lament> i don't think they're as simple as the three things i mentioned
05:58:09 <lament> well, they're on par but somehow clumsier
05:58:16 <lament> plus there's no standard notation for them
05:58:17 <psygnisfive> well, it depends on the language you're implementing it in i suppose
05:59:15 <lament> if your language is objective c, compiling C to it is the simplest way to prove turing-completeness :)
05:59:59 <psygnisfive> ofcourse, if you're objective-c, then doing so is pointless
06:02:12 <lament> compilation is a no-op, yes
06:05:48 <psygnisfive> you might want to try implementing a 5 tuple turing machine model
06:08:39 <psygnisfive> i'd be willing to look at your language and see if its possible on first glance
06:13:07 -!- GreaseMonkey has joined.
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:04:30 -!- olsner has joined.
08:28:30 -!- olsner has quit ("Leaving").
09:14:48 -!- Iskr has joined.
09:36:37 -!- Slereah has quit (Read error: 104 (Connection reset by peer)).
09:36:44 -!- Slereah has joined.
09:39:45 -!- Slereah has quit (Read error: 104 (Connection reset by peer)).
10:03:43 -!- Slereah_ has joined.
10:37:23 -!- GreaseMonkey has quit ("Unisex.").
11:04:53 -!- oklopol has joined.
11:16:44 <Deformative> psygnisfive: It seems it should work, but I am not sure. I know how the universal turing machine works, so I guess I will just attempt to implement one real fast.
11:21:36 -!- oklopol has set topic: (:NAME "#ethoteric" :TYPE (INTERNATIONAL-HUB (PROGRAMMING-LANGUAGETH ETHOTERIC)) :LOGTH "http://tuneth.org/~nef/logth/ethoteric") -- BUT CLICK HERE FOR LINK IF YOUR BROWSER DISLIKES LISP! http://tunes.org/~nef/logs/esoteric.
11:25:28 -!- Sgeo has joined.
11:26:07 -!- fizzie has quit (leguin.freenode.net irc.freenode.net).
11:26:33 <Slereah_> Deformative : Use a Post machine
11:27:06 -!- fizzie has joined.
11:31:39 <oklopol> yeah you can also compile to Ef
11:32:25 <oklopol> ef is my fixed-point language
11:45:26 -!- Sgeo has quit (Remote closed the connection).
12:17:28 -!- Corun has joined.
12:26:45 <Slereah_> It's a primitive Turing machine.
12:27:36 <Slereah_> An infinite tape, two states available for a cell, and the instructions are change to 0, change to 1, left, right and go to state 1 if 0 or state 2 if 1.
12:28:44 <Slereah_> Sort of what Boolfuck is to Brainfuck.
12:32:56 <Slereah_> All the other kids are doing it!
12:43:35 <oklopol> where the fuck is the windows installer i can just fucking click
12:45:30 <oklopol> guess i'll continue doing python
12:45:41 <oklopol> until i find a secretary, that is
12:46:58 <Slereah_> guess i'll continue doing python <- You furry.
13:13:20 -!- Corun has quit ("This computer has gone to sleep").
13:39:40 -!- atsampson has joined.
14:09:24 -!- BMeph has joined.
15:09:38 -!- RedDak has joined.
15:12:14 -!- BMeph69 has joined.
15:15:14 -!- jix has joined.
15:22:13 -!- BMeph has quit (Nick collision from services.).
15:22:56 -!- BMeph69 has changed nick to BMeph.
15:48:38 -!- Judofyr has quit (Read error: 104 (Connection reset by peer)).
15:49:11 -!- Judofyr has joined.
15:51:36 -!- timotiis has joined.
16:00:41 -!- BMeph has quit (Remote closed the connection).
16:11:15 -!- sekhmet has quit (Remote closed the connection).
16:11:18 -!- sekhmet has joined.
16:11:30 -!- BMeph has joined.
16:43:11 -!- AAAAAAue4njxuz has quit (Read error: 104 (Connection reset by peer)).
16:43:19 -!- AAAAAAue4njxuz has joined.
16:48:49 -!- ehird has joined.
16:49:03 <ehird> oklopol's topic owns
16:51:45 <oklopol> ehird: well i put it up out of necessity :)
16:52:06 <ehird> oklopol: did freenode complain
16:52:57 <oklopol> good news, btw, i'm thinking about installing linux on this machine
16:53:06 <oklopol> i assume that's good news :D
16:53:40 <ehird> oklopol: YES, it is
16:54:07 <ehird> oklopol: but plz just get the latest ubuntu because otherwise you'll yell at me about some software not being easily installable or something :p
16:54:36 <oklopol> last time i didn't install it myself, was already there, installed ages ago
16:54:41 <ehird> oklopol: http://www.ubuntu.com/getubuntu/download :P
16:55:16 <ehird> step 1. choose location, step 2. click download, step 3. burn to cd, step 4. boot up cd and choose 'Install' step 5. do what it says step 6. step 6 was eaten by a bird
16:55:29 <ehird> (THE ZONK IS REQUIRED)
16:55:37 <oklopol> another new thing on my todo list, i wanna fail @ making my own OS, haven't done that yet
16:55:57 <oklopol> (i will be dissappointed if i don't fail, ofc)
16:55:57 <ehird> oklopol: oh its quite fun
16:56:03 <ehird> but the base os is uh always the same
16:56:12 <ehird> because there are about 2 tutorials in existance
16:56:15 <ehird> and both of their code is quite similar
16:56:26 <ehird> and you couldn't really deviate without knowing a lot about os dev :p
16:56:33 <ehird> so, yeah, its pretty boring because it's mostly copypasta.
16:56:36 <ehird> and then you get stuck.
16:57:02 <ehird> I'm gonna be ais523
16:58:09 -!- ais523 has joined.
16:58:20 <ehird> I was about to /nick ais523 while nickserv was down :|
16:58:25 <ehird> I guess you saw that, in the losg.
16:58:29 <ehird> And came to DEFEND YOUR IMAGE.
16:58:35 <BMeph> ehird: You forgot the two most important steps on your ubuntu setup!
16:58:45 <oklopol> ais is never here, he just refreshes logs every 10 secs and reads
16:58:46 <ais523> no, only just connected to the Internet
16:58:48 <ehird> BMeph: Sorry, they haven't worked out a business model yet.
16:59:11 <ehird> They don't want to '...' until they have figured out 'Profit'
16:59:26 <ais523> I thought it was ??? not ...
16:59:34 <BMeph> ehird: Well, then, here's your chance to help them. ;)
16:59:59 <ehird> BMeph: Sell their souls to binary driver manufacturers! Oh wait.
17:00:16 <ais523> ah, Ubuntu finally decided to package Firefox 3rc1
17:00:35 <ais523> although I'll keep using Epiphany until 3rc2 is out, probably, because of the fsync bug
17:00:44 <ehird> ais523: i shall wait patiently for debian.
17:00:48 <ehird> fuckin' dinosaurs..
17:01:24 <BMeph> ...is the newest Olympic summer sport! :)
17:01:42 <BMeph> Or is that summer Olympic sport? ;)
17:01:43 <oklopol> i think it's safer to fuck them when they're frozen
17:02:10 <BMeph> oklopol: Ah, but that wouldn't be "sporting," now, would it?
17:04:11 <oklopol> i'm not that sporty myself
17:04:13 -!- Slereah_ has quit (Read error: 104 (Connection reset by peer)).
17:05:27 -!- Slereah_ has joined.
17:05:57 <ehird> so, how zonk is the zonk zonk zonk zonk?
17:17:35 -!- oklopol has quit ("( www.nnscript.com :: NoNameScript 4.2 :: www.regroup-esports.com )").
17:19:57 -!- RedDak has quit (Remote closed the connection).
17:21:52 -!- cherez1 has joined.
17:35:59 -!- Corun has joined.
17:38:19 -!- cherez has quit (Read error: 110 (Connection timed out)).
17:44:32 -!- Slereah has joined.
17:44:33 -!- Slereah_ has quit (Read error: 104 (Connection reset by peer)).
17:50:54 -!- uvanta has joined.
17:51:08 <ehird> * NickServ :Erroneous Nickname
17:51:51 -!- Corun has quit ("This computer has gone to sleep").
18:02:49 -!- ehird has quit (Remote closed the connection).
18:03:28 -!- ehird has joined.
18:09:20 -!- olsner has joined.
18:11:31 -!- kar8nga has joined.
18:15:15 -!- sebbu has joined.
18:26:12 -!- sebbu2 has joined.
18:29:33 -!- oklopol has joined.
18:37:19 -!- sebbu has quit (Read error: 113 (No route to host)).
18:37:20 -!- sebbu2 has changed nick to sebbu.
19:10:11 -!- oerjan has joined.
19:13:38 -!- jix has quit (Nick collision from services.).
19:13:48 -!- jix has joined.
19:27:00 -!- oklofok has joined.
19:29:24 -!- oklopol has quit (Read error: 113 (No route to host)).
19:40:50 -!- AnMaster has changed nick to AnMaster_.
19:40:57 -!- AnMaster_ has changed nick to AnMaster.
19:46:30 -!- Judofyr has quit (Read error: 104 (Connection reset by peer)).
19:46:51 -!- Judofyr has joined.
19:47:45 <ehird> oklofok: infanfoh now
19:48:17 <ehird> ais523: infanfoh is oklofok's inf-d 5-in-a-row
19:48:30 <ais523> how large is the board?
19:48:41 <ais523> infinite in each dimension as well as infinite-dimensions?
19:49:47 <ais523> and are there any rules to negate the first player's advantage?
19:52:34 <ais523> while I used to enjoy 4x4x4x4 noughts-and-crosses, infinite-dimensional five-in-a-row seems hard to keep track of
19:52:46 <ais523> you couldn't even draw the entire board at once, you'd have to keep track of it some other way
19:53:07 <ehird> ais523: his is cli based
19:53:12 <ehird> runs as an irc bot
19:53:16 <ehird> & has no display per se
19:53:18 <ehird> you have to visualize it
19:53:26 <ehird> but it has a mini language for specifying positions, ais523
19:53:27 <ais523> that's why I prefer 4x4x4x4
19:53:31 <ehird> [a b c] for each a in b, c
19:53:41 <ehird> <a b c> a to b, step c
19:53:44 <ehird> and {...} a regular list
19:53:58 <ehird> {50 1 50 2 50 ... 50 10 50 1 50 2 ... }
20:04:42 -!- st01k has joined.
20:07:58 <ais523> wow, there are a lot of people in here
20:08:35 * ais523 wonders about the first in alphabetical order
20:09:56 <ehird> ais523: hes a regular ithink
20:10:02 <ehird> * [AAAAAAue4njxuz] (n=Quendion@145.175.adsl.brightview.com): Aleksander Nonymous
20:10:04 <ehird> quendion is familiar
20:10:14 <ais523> interesting nick, though
20:10:16 <ehird> ais523: I am investigating games programming in Haskell. Not much luck so far ...
20:10:35 <ais523> well, it would need bindings to some graphics lib, probably
20:10:40 <AnMaster> ehird, I think python's pygame may be better
20:10:55 <AnMaster> if you are non-esoteric that is
20:10:57 <ehird> AnMaster: Wow what a revolutionary idea
20:11:03 <ais523> ah, AnMaster, I haven't seen you for ages
20:11:12 <ehird> ais523: I was beginning to get optimistic :(
20:11:15 <ais523> mostly because I haven't been online
20:11:15 <AnMaster> ais523, I have been idling here
20:11:22 <ehird> ais523: there's already opengl and sdl bindings, anyway
20:11:27 <ehird> probably i'll go with sdl because it's simpler
20:11:32 <AnMaster> ais523, how goes the interfunge ;)
20:11:35 <ais523> opengl isn't that complicated
20:11:35 <ehird> but I want a purely-functional approach to sepreate rendering and event handling
20:11:37 <ais523> AnMaster: I've had exams
20:11:39 <ehird> which I think I can do
20:11:50 <ais523> ah, that explains it then
20:12:47 <AnMaster> still have, just one more week
20:12:54 <ais523> but only one exam in that week
20:17:11 <ais523> hmm... I just wrote "business" to mean "extent to which I'm busy"
20:17:40 <ehird> ais523: busyness is incorrect but useful in that case
20:18:00 <ais523> well, I like using correct English even if it produces silly results
20:18:06 <ais523> not sure if it was correct here, though
20:19:07 <ehird> AAAAAAue4njxuz: ha
20:19:20 <ais523> surely it depends on what sort of keyboard you're using?
20:19:29 * ais523 imagines trying to type with one's elbows on an iPhone
20:20:00 <ais523> although they're allegedly hard to type on even normally due to the lack of feedback
20:20:41 <ehird> you get used to it
20:20:50 <ehird> because of its auto-correction you can mostly just hit the right area
20:20:53 <ehird> it has some nifty tricks
20:25:36 <ehird> ais523: humph, I'm going to work on another pseudo-esoteric language.
20:25:43 <ehird> a stack-based, strongly typed a-la haskell and ML language
20:25:47 <ehird> maybe with dependent types.
20:26:20 <AnMaster> AAAAAAue4njxuz, you'd need HUGE keys
20:26:25 <ais523> I've been thinking about writing a Feather bootstrap for a while now
20:26:46 <ehird> cvkftgioufda\zc78dffgftgf8df980c
20:26:54 <ais523> because I'm getting fed up of waiting for a feather interp to spontaneously come into existence
20:27:00 <ehird> gcxoolio ediotglkc
20:27:34 <AAAAAAue4njxuz> AnMaster: only if you want to type accurately, which kind of defeats the point of elbow-typing :p
20:27:50 <AnMaster> AAAAAAue4njxuz, so that is your nick?
20:28:00 <ehird> AnMaster: feather is his infinitely-bootstrapped time-loop language
20:28:04 <ehird> all modifications to the language are always there
20:28:08 <ehird> and the base language creates itself
20:28:20 <ehird> AnMaster: no really
20:28:30 <ehird> AnMaster: it even has a paradox resolution mechanism
20:28:36 <ehird> for when you create a pime taradox
20:28:47 <ais523> AnMaster: a smalltalk-like language that uses retroactive changes to simulate inheritance because it doesn't have classes
20:28:52 <ehird> AnMaster: it's also a prototype-based smalltalk-esque OOP language
20:28:55 <ehird> with no inheritance
20:28:55 <ais523> I haven't written specs like, but I should do at some point
20:29:07 <ais523> objects are created by cloning other objects
20:29:12 <ais523> so you go back in time and alter what they cloned
20:29:50 <ais523> the issue with a code example is that the syntax can be modified at will by the programmer, and probably will be
20:29:57 <ais523> but the initial syntax is designed to be very simple
20:30:15 <oerjan> so this is a grand feather paradox?
20:30:27 <ais523> oerjan: it's not a paradox
20:30:36 <ais523> there's nothing paradoxical about its timetravel model
20:30:44 <ehird> + : 'a 'a -> 'a Num =>
20:31:06 <ais523> {^outputstream write "Hello, world!"}
20:31:12 <ehird> fix : 'a 'a -> 'a ->
20:31:20 <ehird> ais523: suggestion
20:31:23 <ais523> is an example of what a program could look like after you'd implemented a bit of syntactic sugar
20:31:24 <ehird> outputStream, not outputstream
20:31:35 <ais523> ehird: well, it's not part of the language
20:31:44 <ehird> ais523: I'm just saying, you should encourage it
20:31:55 <ehird> ais523: presumably, the base language will come with a Prelude which defines that syntactical sugar
20:32:02 <ehird> so that there's _some_ convenient common base
20:32:05 <ais523> also things like numbers and strings
20:32:09 <ehird> ais523: right, so use thatKindOfNaming for it
20:32:13 <ehird> it fits with smalltalky languages
20:32:54 <ais523> [ ^ | ^ outputStream write [^ helloWorldString ] ]
20:33:09 <ehird> AAAAAAue4njxuz: pleaseBurnInHell
20:33:11 <ais523> isHowItWouldLookBeforeYou'dSugarisedTheParser
20:33:22 <ehird> ais523: interestingButIThinkThatYouNeedaColon
20:33:24 <ais523> becauseToStartWithAllTokensAreSeparatedWithSpaces
20:33:28 <ehird> outputStream write: "Hello, world!"
20:33:29 <ais523> ehird: whereWouldThatBe?
20:33:31 <ehird> because otherwise it gets awkward
20:33:46 <ehird> ais523: oh, um, so it's not smalltalk-like then
20:33:55 <ehird> if you have a thing called a 'function' and you just nab it off an object ... NOT smalltalk-like
20:33:58 <ehird> smalltalk-like = message passing
20:34:16 <ais523> whyCan'tObjectOrientationBeCurried
20:34:36 <ais523> youPassAMessageAndIfItDoesn'tHaveEnoughArgumentsItGivesYouAFunctionSoYouCanSupplyTheRest
20:35:19 <ais523> in Smalltalk, you can write 2 + 2
20:35:24 <AnMaster> where would we be if this contined!?
20:35:30 <ais523> that sends a + message to 2, with the argument 2
20:35:33 <ais523> but it's really 2 +: 2
20:35:59 <ais523> in Feather, assuming you're using a boxed number 2 (you would be normally but you need to deal with unboxed objects during bootstrapping)
20:36:27 <ais523> and that sends a + message to the number 2 and gets back a function that adds 2 to a number
20:36:30 <AnMaster> ais523, go implement it, in INTERCAL
20:36:32 <ais523> not everything is an object, unlike in Feather
20:36:34 <ehird> its inevitable really, ais523
20:36:42 <ehird> you do low-level stuff in the bootstrap
20:36:43 <ais523> actually, I was going to bootstrap it in Scheme
20:36:46 <ehird> and then applications 'clone' the language
20:36:49 <oerjan> AnMaster: THE ANSWER SHOULD BE OBVIOUS
20:36:52 <ehird> and bootstrap away the unsafe operations
20:37:04 <ehird> ais523: also: in place kernel updates!
20:37:13 <ais523> ehird: oh, there was something I was going to ask you
20:37:22 <ais523> you know Haskell has unsafePerformIO
20:37:36 <ais523> the "unsafe" indicating that you're perverting the structure of the language and so should never use it?
20:38:12 <ais523> what should I use as a prefix for an operation which is so ridiculously unsafe that the only use that should ever be used for it is writing safety checks on it to produce a new function that is less unsafe?
20:38:14 <AnMaster> ais523, how do you perform IO safely then?
20:38:26 <ais523> AnMaster: strict evaluation
20:38:43 <ais523> at least, that's for output
20:38:49 <ais523> input is considerably more interesting
20:38:52 <ais523> you have to set up callbacks
20:39:19 <ehird> yourMotherWasAWhoreAreYouSufficientlyOffendedGoodNowYoullNeverTouchThisFunctionBecauseItInsultedYourMotherGoodnight
20:40:31 <ais523> incidentally, the function itself is sort of like become: in Smalltalk, but retroactive to the start of the program and also, whenever you use it you have to ensure that the retroactively modified program doesn't use it for the same purpose again
20:40:48 <ais523> i.e. the only possible use for the function is to modify the program in such a way that you didn't use it
20:40:57 <ehird> i'd just do unsafe
20:40:59 <ais523> veryUnsafeBecome seems to fit well
20:41:08 <ehird> its not for haskell
20:41:15 <ehird> ais523: well, i'd call it primitiveX
20:41:19 <ehird> since presumably it's an internal function
20:41:22 <ehird> and NOT to be called by user code
20:41:29 <ais523> yes, not to be called by user code
20:41:32 <ehird> ais523: primitiveBecome
20:41:37 <ehird> ais523: Haskell uses # for internal things
20:41:39 <AnMaster> ais523, if it would just be used for internal, I'd say either, as ehird suggested primitive, but better: internalBecome
20:41:43 <ehird> e.g. unsafeCoerce# is the internal coercing magic
20:41:47 <ais523> it may be /mentioned/ by user code if you need to invent a different sort of safety check for it
20:41:54 <ehird> ais523: and I# is the primitive int wrapper
20:42:01 <ais523> because there's more than one way to safise it
20:44:54 <ais523> for instance, if you're adding a method or property to an object, you can simply check if it exists and not add it if it does
20:45:10 <ais523> that way, your retroactive modification prevents the same modification being made in the changed program
20:45:44 <ehird> ais523: want to see a dependently-typed stack based program?
20:45:48 <ehird> it uses a type function
20:45:56 <ais523> sounds vaguely interesting
20:46:03 <ehird> ais523: http://pastebin.ca/raw/1033388
20:46:19 <ehird> an example of the type-function formatT:
20:46:24 <ehird> "" formatT -> String
20:46:26 <ais523> wow, that's hard to read
20:46:35 <ehird> "%d" formatT -> (Int -> String)
20:46:39 <ehird> "%s" formatT -> (String -> String)
20:46:49 <ehird> "%s%d abc %s" formatT -> (String -> Int -> String -> String)
20:47:02 <ehird> ais523: its based on the printf from http://www.cs.chalmers.se/~augustss/cayenne/examples.html
20:48:30 <ehird> ais523: admittedly string processing is not something that a stack language excels in
20:48:57 <ais523> is it possible to define printf's type in any strongly typed language?
20:49:07 <ais523> the type of some of the arguments depends on the value of one of them
20:49:13 <ehird> ais523: tada, that's what dependent types are
20:49:17 <ehird> dependent types: types that depend on values
20:49:32 <ehird> ais523: now you might ask -- what about 'format s 3'?
20:49:39 <ehird> How do we know that that is well typed until runtime?
20:49:45 <ehird> ais523: it's simple -- the type system makes you PROVE it!!
20:49:55 <ehird> Just like in haskell which makes you prove things are well-typed
20:50:01 <ehird> ais523: For instance, take this function:
20:50:07 <ehird> myFoo xs = head xs
20:50:08 <ais523> what if you're reading the format string from a file?
20:50:13 <ehird> ais523: I just told you
20:50:15 <ehird> you have to prove it
20:50:19 <ehird> now let me explain ;)
20:50:21 <ehird> myFoo xs = head xs
20:50:29 <ehird> obviously, head [] is not well-typed
20:50:36 <ehird> head operates on _non-empty lists_
20:50:41 <ehird> ergo, the above is a type error
20:50:49 <ehird> myFoo xs = if xs == [] then 3 else head xs
20:51:58 <ehird> ais523: now when you get into dependent types
20:52:02 <ehird> it naturally leads to: Types == values.
20:52:07 <ehird> Types are just values, values are just types.
20:52:12 <ehird> The type language is the programming language.
20:52:27 <ehird> ais523: http://www.cs.chalmers.se/~augustss/cayenne/examples.html Take a look at the 'printf' example. It defines a function in the type system, PrintfType
20:52:34 <ehird> and a function printf, in the value system
20:52:40 <ehird> which utilizes PrintfType to get its type
20:52:49 <ehird> and thus, printf "%d" "abc" gives you a type error.
20:52:53 <ehird> It's a beautiful paradigm and so natural
20:53:36 <ehird> ais523: There are a few problems .. compilation might not halt.
20:53:43 <ehird> But if you do silly things in the type system that's your fault isn't it ;)
20:55:39 <ehird> and then ais523 **DIED**
20:55:46 <ais523> not dead, doing something else
20:55:56 <ais523> but I did read what you wrote
20:55:58 <ehird> ais523: Feather, I hope.
20:56:13 <ehird> ais523: Agoreather
20:56:18 <ais523> and it strikes me that your approach would probably work better in an interpreted language
20:56:40 <ehird> The point is that you can have the static assurance of strong types; if it compilse it runs
20:56:43 <ehird> But it takes it one further
20:56:47 <ais523> ehird: well, I have considered a feathernomic; its defining feature would probably be that all rulechanges were retroactive to the start of the nomic
20:56:53 <ehird> in that you can express _any_ constraint in the type system
20:57:05 <ehird> and the type system helps you by forcing you to prove things that you define
20:57:11 <ehird> which is analogous to .. functions!
20:57:12 <ais523> what if the typechecks are themselves badly typed?
20:57:23 <ehird> ais523: there's an infinite stack of types obviously
20:57:34 <ehird> ais523: think about it
20:57:37 <ehird> its just like expressions vs statements
20:57:42 <ehird> you take regular, fine values
20:57:47 <ehird> and then you add this weird extra language
20:57:53 <ehird> why not just add the same language on another layer?
20:57:54 <ais523> but do you need a precompilation during which you determine the compilation is well-typed?
20:57:58 <ehird> which then has itself as a type layer
20:58:02 <ehird> ais523: well, basically, yes
20:58:05 <ehird> it's like lisp macro expansion
20:58:12 <ehird> you compile down until you get the values compiled
20:58:14 <ais523> and a preprecompilation during which you determine if that is well-typed?
20:58:33 <ais523> that's why I suggested doing it in an interpreted language: to avoid the infinite regress
20:59:00 <ehird> ais523: I think you are misguided. Implementations exist and the languages are developed actually.
20:59:16 <ehird> Agda: http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Main.HomePage
20:59:20 <ehird> ais523: Coq is also dependently typed
20:59:29 <ais523> well, I'm not sure how it would work, but presumably there's some method of avoiding the regress
20:59:40 <ais523> my guess is the higher levels are interpreted, and then it's compiled from there down
21:00:47 -!- Judofyr has quit.
21:13:06 -!- oerjan has quit ("Good night").
21:14:46 <ais523> hmm... whenever I visit a Slashdot article and see that there are no comments, I'm disappointed that there are no comments to read and wait a while, refreshing
21:14:49 <ais523> is this the wrong reaction?
21:15:32 -!- jix has quit ("CommandQ").
21:17:46 -!- Iskr has quit ("Leaving").
21:19:28 -!- jix has joined.
21:19:31 <ehird> ais523: yes, but I do it too
21:19:57 <ais523> besides, my karma's only marginally above excellent
21:20:05 <AnMaster> ais523, yes, you want to make a first comment!
21:20:07 <ais523> so it's not worth doing "FRIST PSOT!!!1" or whatever
21:20:16 <ehird> ais523: my karma on slashdot, iirc, is in the negatives
21:20:23 <ais523> ehird: how did you manage that?
21:20:47 <AnMaster> ais523, make a *good* first comment
21:20:55 <ehird> ais523: said some crap
21:20:58 <ais523> AnMaster: impossible, you have to spend thinking time to do that
21:21:03 <ehird> I don't like slashdot :-)
21:21:08 <ais523> I've made good early comments, though, that have been moderated up to 5
21:21:16 <ais523> and the article was blank when I started making them
21:21:29 <ais523> but because I put thought into them there were something like 7 or 8 comments before mine
21:21:55 <AnMaster> oh you mean blank with comments
21:22:18 <ais523> I mean no comments, yes
21:22:29 <ais523> although if you're fast enough, and I have been sometimes, the read more... link is a 404
21:22:44 <ais523> because the articles don't always come up at the same time on the main page and elsewhere
21:23:05 -!- RedDak has joined.
21:28:54 -!- uvanta has changed nick to HanDongSeong.
21:48:17 -!- cherez1 has changed nick to cherez.
22:09:07 -!- olsner has quit ("Leaving").
22:15:51 -!- kar8nga has left (?).
22:16:29 -!- BMeph has quit ("Time for me to go home").
22:16:59 -!- BMeph has joined.
22:25:20 -!- jix has quit ("CommandQ").
22:26:53 -!- ais523 has quit ("(1) DO COME FROM ".2~.2"~#1 WHILE :1 <- "'?.1$.2'~'"':1/.1$.2'~#0"$#65535'"$"'"'&.1$.2'~'#0$#65535'"$#0'~#32767$#1"").
22:34:36 -!- Corun has joined.
22:50:13 -!- RedDak has quit (Remote closed the connection).
23:12:18 -!- BMeph has quit (Read error: 104 (Connection reset by peer)).
23:40:19 <oklofok> what does ais's quit message do?
23:41:20 <ehird> put: (1) DO COME FROM ".2~.2"~#1 WHILE :1 <- "'?.1$.2'~'"':1/.1$.2'~#0"$#65535'"$"'"'&.1$.2'~'#0$#65535'"$#0'~#32767$#1"
23:43:18 -!- HanDongSeong has quit ("If you're seeing this message, it's probably XChat's fault.").