00:00:21 *Main> System.IO.UTF8.putStrLn $ pretty idL 00:00:21 (λα : (α : ★) → (β : α) → α. α) 00:00:30 *Main> System.IO.UTF8.putStrLn $ pretty consL 00:00:31 (λα : (α : ★) → (β : ★) → (γ : α) → (δ : β) → (ε : ★) → (θ : (ζ : α) → (η : β) → ε) → ζ. (λβ : (ι : ★) → (κ : θ) → (μ : ι) → (ν : ★) → (π : (ξ : θ) → (ο : ι) → ν) → ξ. (λγ : (ρ : ο) → (σ : π) → (τ : ★) → (χ : (υ : ο) → (φ : π) → τ) → υ. (λδ : (ψ : φ) → (ω : ★) → (γ′ : (α′ : υ) → (β′ : φ) → ω) → α′. (λε : (δ′ : ★) → (η 00:00:31 ′ : (ε′ : ω) → (ζ′ : α′) → δ′) → ε′. (λζ : (κ′ : (θ′ : γ′) → (ι′ : δ′) → η′) → θ′. ζ γ δ)))))) 00:00:34 -!- MizardX- has joined. 00:01:51 -!- adam_d_ has quit (Quit: Leaving). 00:03:14 -!- MizardX has quit (Ping timeout: 276 seconds). 00:03:33 -!- MizardX- has changed nick to MizardX. 00:07:05 MissPiggy: in a dependent lang the function arguments to church numerals don't have to be a->a do they 00:07:12 pretty? 00:07:13 they just have to be (something which includes b)->b 00:07:24 Sgeo: prettifies a dependently-typed lambda calculus AST 00:07:38 * Sgeo is already confused 00:08:46 Sgeo: just go along with him 00:08:50 *her 00:09:29 well that's a subtype of b->b isn't it 00:10:28 hïrm 00:11:00 oerjan: right 00:11:04 *Main> System.IO.UTF8.putStrLn $ pretty (church 0) 00:11:04 (λα : (α : ★) → (γ : (β : α) → α) → (δ : α) → α. (λβ : (ζ : (ε : δ) → δ) → (η : δ) → δ. (λγ : (θ : ε) → ε. γ))) 00:15:11 Something's broken... 00:18:22 *Main> System.IO.UTF8.putStrLn $ pretty (church 50) 00:18:22 (λα : (α : ★) → (γ : (β : α) → α) → (δ : α) → α. (λβ : (ζ : (ε : δ) → δ) → (η : δ) → δ. (λγ : (θ : ε) → ε. (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β (β γ))))))))))))))))))))))))))))))))))))))))))))))))))))) 00:21:21 *Main> System.IO.UTF8.putStrLn $ pretty trueL 00:21:21 (λα : (α : ★) → (β : α) → (γ : α) → α. (λβ : (δ : γ) → (ε : γ) → γ. (λγ : (ζ : δ) → δ. β))) 00:21:21 *Main> System.IO.UTF8.putStrLn $ pretty falseL 00:21:21 (λα : (α : ★) → (β : α) → (γ : α) → α. (λβ : (δ : γ) → (ε : γ) → γ. (λγ : (ζ : δ) → δ. γ))) 00:22:01 -!- BeholdMyGlory has quit (Read error: Connection reset by peer). 00:22:25 "As an alternative to the encoding using Church pairs, a list can be encoded by identifying it with its right fold function." 00:22:26 Me likey. 00:22:40 can you define foldl with foldr? 00:24:17 yes 00:24:31 alise but why would you... 00:24:55 MissPiggy: if a list is defined as its foldr... 00:25:01 what oerjan said 00:25:10 defining things as their natural functions is a nice thing 00:25:20 like Maybe a is b -> (a -> b) -> b 00:25:28 Either a b is (a -> c) -> (b -> c) -> c 00:25:33 (a,b) is (a -> b -> c) -> c 00:25:34 etc 00:25:40 it's one of those anamorphism or catamorphism things 00:25:43 oerjan: what's the definition btw? 00:25:51 * oerjan cannot remember which is which 00:26:02 hm lessee 00:26:26 foldl' f b0 as = foldr (\a k b -> k (f b a)) id as b0 00:26:27 apparently 00:26:45 why the ' ? 00:26:51 that's what the LtU person called it 00:26:53 just not to clash 00:26:55 not for strictness afaik 00:26:58 oh 00:26:59 they failed :P 00:27:01 (at not clashing) 00:27:07 heh 00:27:39 i'm beginning to realise why nobody uses the dependently-typed lambda calculus as a core language 00:27:44 (it's frickin' verbose and opaque!) 00:28:01 um 00:28:09 you cant encode data types by the folds 00:28:20 you can represent a list as its foldr 00:28:28 it doesnt' work 00:28:31 yes, it does 00:28:42 sure you can. it's how it's done in System F iirc 00:28:48 map, foldl, head, tail, ... can all be implemented with juts foldr 00:28:50 *just 00:29:03 also: http://en.wikipedia.org/wiki/Church_encoding#Higher-order_function 00:29:50 MissPiggy: also is it just me or does prolog solve the expression problem? 00:29:51 maybe 00:30:10 prolog has no static types. 00:30:20 without which, it is much easier 00:30:24 iiuc 00:30:50 I don't think there's any point me linking to a research problem that proves what I am saying if you already know that I am wrong 00:31:23 MissPiggy: well, do link 00:31:34 but i'm fairly sure oerjan and wikipedia, and facts back me up on this 00:32:13 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.4355 00:32:45 note that this foldr encoding of lists applies to when lists have all elements the same type, like in haskell 00:32:50 MissPiggy: i'm just talking about lists 00:33:04 yeah I knew it was pointless 00:33:10 sigh 00:33:20 i don't think you understand what i'm saying 00:33:21 data Nat : * where 00:33:22 Z : Nat 00:33:25 S : Nat -> Nat 00:33:28 data List : * where 00:33:30 nil : List 00:33:37 cons : a -> List -> List 00:33:41 same thing 00:34:03 * coppro knows how to bug alise... hehehe 00:34:12 How? 00:34:31 MissPiggy: so, are you saying that map isn't implementable with just foldr? what about foldl? head? tail? 00:34:41 by insisting that C# solves the Expression Problem 00:34:49 you can do whatever the fuck you want in haskell or untyped lambda calculus or wikipedia 00:34:57 what does that have to do with it 00:35:41 coppro: >_< 00:35:51 it comes close 00:35:53 MissPiggy: because you are being opaque about what you are actually trying to state to me 00:36:07 coppro: can you add new methods and have them work on existing members of a type hierarchy? 00:36:20 alise: Yes, they're called extension methods 00:36:27 I think it's more a case of you already have your mind made up 00:36:32 they're just glorified functions, but okay 00:36:38 that doesn't really count :P 00:36:47 MissPiggy: I haven't and I'm trying to get the information out of you, dammit 00:37:02 they are 00:37:02 and you seemed to read an entire research paper in the amount of time it takes to read its title 00:37:13 MissPiggy: um so whether you can define a data type using a foldr might depend on your type system. what does that have to do with what we are saying? 00:37:22 but does the semantic difference of what is and isn't a member of a type matter? 00:37:23 MissPiggy: i read the abstract 00:37:29 usually that summarises what the paper concludes. 00:37:35 other than the verbosity 00:37:39 coppro: yes 00:37:49 alise: explain 00:37:56 coppro: access to private fields 00:38:02 QED 00:38:24 it's equally clear that in the System F type system people _have_ defined list types as their corresponding fold types 00:38:33 this thread of discussion has got murky and clouded with assumptions so lets clear it and we can start again 00:39:00 alise: that isn't required 00:39:09 coppro: well nothing is required 00:39:17 the expression problem doesn't reduce a language's power 00:39:21 it reduces its expressivity 00:39:45 * coppro wonders why the idiot decided to refer to it as being solved, when it really isn't 00:39:59 I'd argue prototype systems come closest to solving it 00:40:01 What idiot? 00:40:09 The author of the .txt file? 00:40:10 alise: Wadler 00:40:13 O_O 00:40:16 You just called Wadler an idiot. 00:40:50 Firstly, Wadler is a great computer scientist who came up with using monads in programming and many aspects of Haskell's design. 00:40:51 he was an idiot when he decided to refer to it as being solved 00:40:54 or solvable 00:41:00 Secondly, he didn't. He presented *one solution*. 00:41:11 It allowed you to add both rows and columns. 00:41:13 That is a solution of the problem. 00:41:21 It may not be the best or even a good solution, but it is a solution. 00:41:40 in that case I contend that C# has solved it 00:42:05 No. 00:42:06 Private fields. 00:42:53 I contend that those do not matter 00:43:28 Nothing matters. 00:43:34 It is a problem of convenience and expressivity, not power. 00:43:43 So either obey all the rules or obey none. 00:43:54 If it wasn't about private fields, *every* OOP language would solve it. 00:44:04 (In an awful, kludgey way, of course.) 00:44:21 you have to "add new cases to the datatype and new functions over the datatype" 00:44:24 Summary: In lambda caculus you can define data types (including higher order ones like the syntax of lambda caclculus itsself using the Scott encoding, in Haskell you can't use this because it doesn't typecheck but data types are isomorphic to the folds (but the algorithmic complexity of functions you define on the fold version is limited), in dependently typed calculus you can't use the fold encoding because you can't do induction on these types. 00:44:28 coppro: Anyway, if you add an extension method to a subclass, do you have to add it to all superclasses too? 00:44:43 Summray: In untyped lambda caculus**** 00:44:45 If you add an extension method to a superclass, do you have to make separate definitions for each subclass? If not, then it is not solved. 00:44:48 alise: Actually, that I'm not sure about, and would be fatal to the Expression Problem 00:44:52 alise, oerjan ^ 00:44:54 but access to private members is not fatal 00:45:30 Interestingly enough, prototype systems take it one step further 00:45:55 i just spent about half an hour to an hour shoveling snow 00:46:11 par for the course 00:46:22 GRAR UPPER BODY STRENGTH 00:46:26 HULK SMASH SNOW 00:46:58 MissPiggy: kay :P 00:47:03 you are the snow shovelar! 00:47:11 coppro: But yes, I just realised that's why it doesn't solve it. 00:47:13 prototype systems let you define new functions over individual objects 00:47:20 -!- Wareya has quit (Read error: Operation timed out). 00:47:22 coppro: In a real-life table of numbers, 00:47:24 i'd shover your snow ;o 00:47:28 I typed that all out and you're not even going to read it? 00:47:31 you can't just add a column, put one number in, and pretend all the rest are that number 00:47:37 You have to fill in each separately, considering each row 00:47:59 MissPiggy: I read it 00:48:10 MissPiggy: why do you assume I did not? 00:48:16 ah, true 00:48:32 * coppro motions quietly in the direction of Python 00:48:33 coppro: admittedly, normal OOP systems fail at this with rows too by inheriting methods; but that's less bad, since it's just one row being affected 00:48:41 rather than a nuclear holocaust of oppression as in adding a column 00:49:16 alise: why does inheriting methods screw it up? 00:49:25 wait, it doesn't 00:49:36 with the column fuckup you enter one and it magics into the other rows 00:49:41 but with method inheritance, there's no entering+copying 00:49:44 it's just regular inheritance 00:49:45 ok 00:50:10 Incidentally, language implementations with a solution of the expression problem are godly in their ease-of-organisation. 00:50:25 ok, here's a fun one 00:50:37 Erlang 00:50:41 Adding a new construct? You can do it in one module: add a row to the AST type, implement all the columns (like "compile", "prettyprint"), add it to the parser, and you're done. 00:50:44 oerjan? 00:50:47 (note: I know it doesn't solve it. I'm asking you to describe why ont) 00:50:47 -!- Wareya has joined. 00:50:48 *not 00:50:58 alise because you didn't even argue 00:51:00 It becomes organised by feature, not by phase. 00:51:09 MissPiggy: because you're probably right :P 00:51:18 coppro: Erlang isn't strongly-typed; mu 00:51:30 well. you can't add pattern-matching cases to a function in erlang, too 00:51:41 so even if you arbitrarily said {foo,2} is your new row, you can't fill in the columns 00:51:47 yeah, it fails pretty hard 00:51:54 funny for a functional language though 00:52:04 adding new types is the easy bit 00:52:13 well, since it's not statically typed you can think of it as being able to add rows 00:52:18 it's just that you don't have to declare the rows you add :) 00:52:19 MissPiggy: well as i said it means it doesn't work in all type systems. perhaps it's a general problem for all dependent ones, i don't know. 00:52:27 er 00:52:28 wait 00:52:28 no 00:52:30 it can add columns 00:52:32 but definitely not rows 00:52:33 right 00:52:35 like most functional languages 00:52:56 the expression problem only really makes sense with static typing 00:53:26 coppro: i was expecting you to be more "coool" at my thing about language implementation organisation :( 00:53:45 sorry 00:53:53 ehird 00:53:53 :P 00:53:57 alise* 00:54:02 ha, i was just about to 00:54:32 are you considering designing a language which has a very easy solution to the expression problem? 00:54:39 food -> 00:55:04 augur: i'm considering including my nice syntax for my solution in my language 00:55:08 and making _all_ types tables 00:55:17 (although of course you have to export the table part to get it extensible by others etc) 00:55:34 all ADTs that is 00:55:46 I wonder if the ability to subclass could be considered a requirement 00:55:58 no, just extend the type 00:55:59 hm 00:56:10 subtyping in OOP extends the parent type, because you can use the subclasses as their parents 00:56:11 or have type extensions of some sort 00:56:16 yeah 00:56:18 yes 00:56:19 that's adding rows 00:56:22 well 00:56:26 adding row = extending type + filling in columns 00:56:35 adding column = making function + filling in rows 00:56:40 with covariance or contravariance? 00:56:49 COMONADS AND CONTRAMONADS 00:56:57 coppro: I don't see why? 00:57:04 alise: no, I mean which 00:57:09 er I was thinking of the wrong meaning of covariance :D 00:57:21 coppro: no, all the extensions are considered equal 00:57:29 subtyping in OOP just happens to do this, it isn't the optimal way 00:57:36 the optimal way is simply adding constructors to an existing data type 00:57:37 subtyping in OOP is covariant 00:57:41 (usually) 00:57:50 yes, but it doesn't matter for the expression problem 00:57:56 but it does 00:57:58 subtyping is a more general operation than what you need for the expression problem 00:58:05 with the expression problem, all are = 00:58:27 what does one define as "adding new cases to the datatype"? 00:58:57 data Foo a = Abc Int a 00:59:01 data Foo a = Abc Int a | Bar a a 00:59:04 data Foo a = Abc Int a | Bar a a | Quux Int String 00:59:32 * alise realises something 00:59:43 alise: Why doesn't simple composition not qualify? 00:59:46 my language probably has almost as many features that almost all other languages don't have, as common features 00:59:48 *does 00:59:55 coppro: it does i think? 01:00:14 well you just said that extension was necessary 01:00:22 well it has to extend the original type 01:00:23 unless we were talking about different definitions of extension 01:00:28 because you fill in the columns 01:00:30 people in haskell are mean 01:00:32 and you can't change the type of the columns 01:00:34 #haskell 01:00:35 it's an overloaded word I think 01:00:39 dependent types, mixfix operators, extensible syntax, partiality as an effect, heavy unicode usage, 01:00:47 solution to the expression problem, 01:00:48 ... 01:01:05 alise: what do you mean "fill in the columns"? 01:01:17 when you add a new row 01:01:24 you have to implement all the functions (columns) 01:01:25 for that row 01:01:40 again, think of a real table of numbers 01:01:49 I don't think that's a requirement 01:01:49 if you add a row, you have to fill in the values for its columns 01:01:55 since many functions can't be implemented 01:01:59 if you add a column, you have to fill in the values for its rows 01:02:03 coppro: all the functions previously added 01:02:04 the columns 01:02:12 * alise is beginning to suspect you don't understand the problem... 01:02:14 -!- coppro has left (?). 01:02:20 uh, bye. 01:02:21 -!- coppro has joined. 01:02:23 wb 01:02:27 did you miss anything? 01:02:29 alise: I do understand it 01:02:30 no 01:02:34 wait 01:02:39 do you have the link to my explanation? 01:02:41 I'll show what I mean 01:02:44 no 01:02:45 I don't 01:02:54 ok 01:03:14 AFAICT, we're currently arguing over the specification of the problem 01:03:17 i need the explanation though :P 01:03:22 i could search the logs I guess 01:03:34 coppro: well, I'm 99.9% sure I've described the problem correctly 01:03:48 alise: I'll wait on your explanation before saying more 01:03:55 just to check 01:03:59 you have read http://pastie.org/812459.txt?key=cadkhg4ho0qiceepz1a7w right? 01:04:06 might be good to read it again :P 01:04:12 (I wrote it) 01:05:00 slight hinting + greyscale antialiasing makes linux typography okay, yay. 01:05:49 alise: yes, I agree 01:05:59 with the antialiasing thing? 01:06:05 no, your explanation 01:06:08 ah :P 01:06:15 however, I also see our disagreement 01:06:28 you're considering it as an isolated case; I'm considering every function and type as a whole 01:07:06 ? 01:07:10 add more jargon to that 01:07:13 it's too vague 01:07:14 e.g. there is an comparison function which is defined for numbers, but not for lists 01:07:30 whereas there is a function to get the first element of a list that is not defined for numbers 01:08:05 a table is a type, by the way 01:08:10 rows = members of that type 01:08:13 columns = functions on that type 01:08:15 ah 01:08:20 okay, that's what I was missing 01:08:23 rows are data, columns are functions 01:08:24 tables are types 01:09:54 now things make more sense :) 01:10:36 yeah the "some functions aren't implementable" thing was confusing me 01:11:02 also, note that not every function on a type needs to be a column; if it doesn't access the data directly and is just a composition of columns and other non-column functions, it doesn't change definition depending on the row 01:11:14 hey alise, will you be on next week? 01:11:21 wend 01:11:25 MissPiggy: End, yes; why? 01:11:35 well just wondering like if you aren't 01:11:39 then ? 01:11:48 coppro: this adds slight awkwardness to the typical functional style because you have to declare column functions specifically; I'm considering inferring it 01:12:00 (pattern match = Damn nigga, you sum columnic function) 01:12:15 MissPiggy: Then what? You mean if they find out and imprison me in a fortress for 100 years? 01:12:52 okay so you're not worried 01:13:41 Not particularly. They know I can program and like being on the computer (which I wave away with "talking on IM? yeah, yeah, that. no, not Facebook") but I don't think they know I have any sort of web prescense, so them googling for me is unlikely 01:14:00 If they don't do that, how will they find out? The incriminating thoughts have been in my head since the first few days and they don't seem to have read them yet. 01:14:34 If I'm not on this week or next week, well... what can you do? Nothing, really. 01:14:42 Rest assured I won't be personally giving up, so... 01:15:52 We'll just assume your Finnish internet connection isn't set up :P 01:16:27 Internet connection is the only thing going for Finland over Sweden and Norway. 01:16:37 I'm adamant about not working for the military, so it's out :P 01:16:52 (Even though by 18 I'll be a senior professor of awesome at MIT.) 01:17:21 I thought you weren't going to the USA? :P 01:18:34 All the excellent CS universities are in America. I could, at least, stand Massachusetts. :-P 01:18:48 Also note that I may have been joking a wee bit, what with the senior professor of awesome thing. 01:18:56 *gasp* 01:19:12 clearly this is the difference between male and female ehird 01:19:38 yeah the male one never joked 01:19:39 Yes; female alise would never be promoted to Senior Professor of Awesome because of SEXISM 01:19:56 Also, hey, who says I'm female! Just because I'm referring to myself with female pronouns! 01:20:10 It's sexism to mandate that only one sex can use one set of pronouns. 01:20:20 it's the (s)h/it, man 01:25:37 Why did classic Clearlooks become modern Clearlooks? 01:25:40 Old Clearlooks is far prettier. 01:33:40 alise: they'll have to create that professor for you, i think 01:34:47 Professor. Ingredients: 50 bananas/day. 25 cups of coffee/day. 1 Ph.D. Mix until of a frazzled and messy consistency. Cook for 30 minutes at 30 Celsius. 01:35:15 or, if a physicist, at 300 K 01:36:35 yes physicists are cold, horrible people 01:36:37 is that what you meant? 01:36:49 3.15 degrees make all the difference 01:37:02 hmm, so the difference between a physicist and a mathematician is ~pi 01:37:07 makes sense. 01:37:20 -!- Asztal has quit (Ping timeout: 258 seconds). 01:38:31 * coppro cackles 01:38:50 wat. 01:39:07 I'm trying to freeze the physicists 01:39:50 xD 01:40:07 yeah 26.85 degrees is freeeeeeeezing 01:40:13 I know I'll never get rid of their energy entirely, but I'll get rid of what I can 01:40:27 coppropy 01:40:50 then I shall design a mysterious and inexplicable device with their zero-point energy 01:42:28 hmm... in what language should I write my text visualizer? 01:45:07 Haskell. 01:45:18 cobol 01:45:19 "text visualizer"? 01:45:20 Already had your reply written down 01:45:26 I already have one of those 01:45:31 The whole program essentially boils down to "vis s = map tile s", after all. 01:45:43 Indeed, with FRP, you could write literally that. 01:45:46 to start, yeah 01:46:04 Okay then, "vis tiles s = map (tile tiles) s". 01:46:50 yes, I get it :P 01:46:59 I'm strongly considering Haskell 01:47:00 Well, it's not "to start with", it's pretty close to all you need. 01:47:09 alise: I intend to add more features 01:47:15 Of course, but the actual tiling part. 01:47:17 screw Unix 01:47:29 coppro: If you do, please do consider using an FRP toolkit. 01:47:37 You don't have to worry about updating the rendering on its changing or anything. 01:47:42 alise: Yes, that seems like a good idea :) 01:47:43 (FRP is basically event-based programming, but functional) 01:48:10 coppro: Unfortunately, most FRP implementations suck. :-) 01:48:28 I don't know if GuiTV lets you do arbitrary graphics, but look at http://www.haskell.org/haskellwiki/TV for the sort of thing that would help updating 01:48:58 (TV is conal's plaything, and conal is one of the main FRP dudes; he was writing papers about it from the start) 01:49:16 coppro: So what kind of features are you considering? 01:49:20 Here's something that would be cool: 01:49:47 alise: changing tile images based on surroundings, possibly editing 01:49:53 You could tell it to run the command "nethack", with a definition file that says the area of the screen (coords of the map) is to use tileset foo, and the rest is to use tileset (a simple bitmap font). 01:50:02 It'd interpret the vt100 codes and send your keypresses, and voila! 01:50:06 yeah, that was on the 'lofty goal' bit 01:50:09 Graphical nethack in a few lines and some drawing! 01:50:14 vt100 codes are very simple, so 01:50:18 yep 01:50:23 was thinking that /exact/ thing, actually 01:50:23 you could even use termcap/whatever to make them send ones easier for you 01:50:33 not that I'd actually use it for nethack 01:50:50 writing apl :P 01:50:56 :P 01:51:06 given a program that compiles ascii characters to apl chars 01:51:19 you could arrange the apl chars to the alphabet etc on your keyboard to your liking like the old apl keyboards, and just type away 01:51:47 I like APL 01:51:51 where should I start with actually learning Haskell Syntax? 01:52:04 coppro: You should learn Haskell in one go. :-) 01:52:06 coppro, f x y z is what you'd normall write like f(x,y,z) 01:52:11 alise: yes, but where 01:52:14 http://learnyouahaskell.com/ is an excellent starting point. 01:52:14 except that its ACTUALLY (((f x) y) z) 01:52:25 thank you for telling me what currying is 01:52:29 It's practical, simple to understand and amusing. 01:52:36 I like the elephant 01:52:37 MissPiggy: coppro is rather beyond that stage 01:52:42 coppro thank you for learning the first thing about haskell syntax 01:53:02 I also happen to sort-of understand monads 01:53:06 coppro: learn you a haskell doesn't actually explain monads yet, but surely you've picked up what a monad is by now? 01:53:08 ha 01:53:15