01:17:26 what's the name for the operation which converts a value into a type (e.g. in dependently-typed languages)? I'm vaguely remembering "lift" but am not sure that's correct 01:18:28 -!- amby has quit (Quit: so long suckers! i rev up my motorcylce and create a huge cloud of smoke. when the cloud dissipates im lying completely dead on the pavement). 01:23:41 I don't know? 01:25:24 ais523: are you looking for the reify/reflect pair that's illogically named? 01:26:25 (reify would be the one that creates a type from a value; I find that illogical because the values are supposed to be concrete and the reflections immaterial) 01:39:55 int-e: so I'm trying to implement the "scoped generic" thing that b_jonas and I were talking about earlier – what I'm doing is writing a library in which a value that exists at runtime can be used as a generic parameter in the type system, meaning that types parameterised the same way are always referring to the same value 01:40:21 and the language doesn't have a generic like that, so the library takes a value and creates a type to represent it 01:40:39 and I was wondering what the standard name for that is (and if it made enough sense to use) 01:42:45 here's an example use of that terminology: https://hackage.haskell.org/package/reflection-2.1.8/docs/Data-Reflection.html#v:reify (`reflect` has a friendlier type but isn't the operation you want) 01:43:43 ais523: unless I'm misunderstanding but what you just wrote is still in line with that 01:43:44 does "s :: *" mean that s has a simple kind, i.e. is a type? 01:44:03 yeah 01:45:00 I think that might be the operation I want, but will need to really concentrate to make sure 01:49:14 OK, so this is basically the operation I want, although it's implemented slightly differently – in my case values of arbitrary types can be converted to types and the only thing you can do with the resulting types is convert them to values, whereas with Data.Reflection it generates particular types which aren't opaque and you can match on the structure of the type (which means that it only works for certain types of «a») 01:49:31 and I think that difference might be enough to cause a difference in the naming (in any case, I am not a fan of those names) 01:51:24 ais523: Nah, the only thing that `reify` allows you to do with `s` is use the `Reifies` class instance, and that only gives you back the value. 01:51:32 actually I think my API is more like that of Given than Reifies 01:52:04 Actually I thought *you* wanted to deconstruct the resulting type, so the `reflection` package would fall short. 01:52:18 But you only asked for a name and that would still apply. 01:52:23 right 01:52:35 I assumed there was a standard name 01:52:37 but maybe there isn't 01:53:18 Maybe these names are only used in the Haskell niche. I wouldn't be terribly surprised. 01:54:28 hmm, maybe something like "value_as_type" would be clear to people who aren't used to dependently typed languages 01:54:45 (it is certainly less ambiguous doing it that way round than an OCaml-ish "type_of_value"!) 01:58:54 ais523: Oh. Here's the thing about deconstructing that `s` type... *if* that type was actually a standard type like Either (Int, Bool) (Char -> [Bool]) then yes, you'd be able to deconstruct it using type class instances. But conceptually it just makes up an entirely new, anonymous type. 01:59:45 And *actually* it relies on type erasure and gets away with not creating a type at all, just a class dicitionary for it that encapsulates the given value. `Given` does exactly the same thing but a but more honestly. 02:01:40 hmm… the variance seems wrong here 02:02:29 ah, no 02:02:49 I think I'm confused about how forall works in Haskell 02:03:18 or maybe => 02:05:48 forall s. a means the caller provides s, and the result type is a. Except Haskell doesn't allow that unless `s` can be determined from the type `a`. So you end up with forall s. Proxy s -> a shenanigans for that. 02:06:02 I'd expect "give" to take two arguments (via currying): an argument of an arbitrary type a, and a polymorphic function that can take a type parameter of any type with the "Given a" typeclass to produce a result of an arbitrary type r, returning r 02:06:17 and I think it actually does that and I just misread the syntax 02:06:32 operationall, Reifies s a => is also a function; the caller provides a class dictionary for the given s and a. 02:07:16 and you end up with (forall s. r) -> r because there's no type-level `exists`; it has to be encoded like that instead (or tucked away into a GADT I suppose) 02:09:00 it *is* a horrible looking type 02:10:08 Especially if you consider the counterpart `reflect :: proxy s -> a` that is largely unencumbered by these restrictions (still "suffers" from having no type applications... well GHC added them but that happened very recently) 02:16:48 is it correct to think of => as being like a function arrow for a function that takes a type as argument, just like -> is a function arrow for a function that takes a value as argument? 02:22:13 Well the thing to the left of => tend to be class dictionaries (more generally constraints), so they aren't types. And the forall s. a syntax doesn't have an arrow at all. 02:25:16 right 02:26:57 I was expecting a type for "give" like «forall a r. a -> (forall s where s :: Given a. r) -> r» but that might not be easily expressible as a Haskell type 02:30:03 Well, the type of `given` really makes no sense logically. 02:32:07 Like if you take the usual rules of haskell, you can only ever have one instance of `Given Int`, say, `Given Int where given = 42`. But using `given` you can (and essentially have to) violate this constraint. 02:32:39 Err, I mean `give` 02:33:08 I also meant `instance Given Int where given = 42` 02:34:30 But if you want a logical type, and express it in Haskell, you end up with `reify` or something that closely resembles it, with the model that each time you use it with a new value, you get a different `s`. 02:34:51 right 02:35:03 I guess what i'm trying is indeed more like «reify», then 02:35:58 doing this in Rust has one major advantage, which is that Rust already has types that are (e.g.) different each time round a loop 02:36:59 but unfortunately the types differ only in the lifetimes, which are erased at runtime, so without language changes, you can only implement the equivalent of «reflect» for finitely many types at a time (so it doesn't work in recursive contexts) 02:46:14 did the context leading up to it involve https://doc.rust-lang.org/stable/std/thread/fn.scope.html ? 02:47:36 (Obviously that doesn't encode values. it's just the one place in Rust that I'm aware of that conjures a lifetime from thin air and (ab)uses it as a tag.) 02:49:57 Maybe I should try to read context. That definitely won't happen tonight though. 02:50:21 int-e: sort of; using lifetimes as tags is a known technique 02:50:58 http://ais523.me.uk/blog/scoped-generics.html is a good source for where all this came from, and probably more understandable than the IRC logs (but it's long enough that you won't want to read it tonight) 02:51:06 :t runST 02:51:07 (forall s. ST s a) -> a 02:51:32 (earliest use of this particular trick in Haskell... well as far as I'm aware) 02:51:56 there's some discussion of the history of using lifetimes as tags in there (which the Rust community calls "generativity") 02:51:56 [[///]] https://esolangs.org/w/index.php?diff=159964&oldid=147306 * Tanner Swett * (+0) Update my name 04:29:11 -!- ^[ has joined. 04:35:49 [[Category:Instruction list pointer]] N https://esolangs.org/w/index.php?oldid=159965 * BestCoder * (+178) Created page with "when an esolang uses a list of instuctions and commands to move a cursor in the list of instructions and run them to artifically decrease "instruction count", example [[Example]]" 04:38:48 [[Example]] N https://esolangs.org/w/index.php?oldid=159966 * BestCoder * (+265) Created page with "example for a category == commands == a - moves pointer to left d - moves pointer to right s - runs command at pointer == list == list: 1234 1 - prints 1 2 - prints 2 3 - prints 3 4 - prints 4 also pointer wraps around [[Category:Instruction list pointer]]" 04:40:59 [[Category:Instruction list pointer]] https://esolangs.org/w/index.php?diff=159967&oldid=159965 * BestCoder * (+41) 04:45:04 [[Template:Stub]] https://esolangs.org/w/index.php?diff=159968&oldid=143707 * BestCoder * (+1) 04:47:19 [[Template:Stub]] M https://esolangs.org/w/index.php?diff=159969&oldid=159968 * Corbin * (-1) Undo revision [[Special:Diff/159968|159968]] by [[Special:Contributions/BestCoder|BestCoder]] ([[User talk:BestCoder|talk]]): No, I thiink iit was fiine before. 04:48:20 [[Template:Stubnoinfo]] https://esolangs.org/w/index.php?diff=159970&oldid=154752 * BestCoder * (+3) 04:50:32 [[Template:Deadlink]] https://esolangs.org/w/index.php?diff=159971&oldid=30797 * BestCoder * (+20) 04:52:04 [[Template:Stubnoinfo]] https://esolangs.org/w/index.php?diff=159972&oldid=159970 * Corbin * (-217) Remove several layers of vandalism. 04:52:31 [[Template:Deadlink]] M https://esolangs.org/w/index.php?diff=159973&oldid=159971 * Corbin * (-20) Undo revision [[Special:Diff/159971|159971]] by [[Special:Contributions/BestCoder|BestCoder]] ([[User talk:BestCoder|talk]]) 04:53:58 [[Category talk:Instruction list pointer]] N https://esolangs.org/w/index.php?oldid=159974 * Corbin * (+273) Created page with "This category was created without discussion. As such, it might be deleted. Next time, please follow the [[esolang:policy]] and start a discussion on [[esolang talk:categorization]] first. Thanks! ~~~~" 05:09:12 [[]] https://esolangs.org/w/index.php?diff=159975&oldid=158461 * Xyzzy * (+504) 05:11:07 [[User talk:Xyzzy]] https://esolangs.org/w/index.php?diff=159976&oldid=158901 * Xyzzy * (+143) 05:12:58 [[User:BestCoder]] https://esolangs.org/w/index.php?diff=159977&oldid=159712 * BestCoder * (+41) 05:13:27 [[User:BestCoder]] https://esolangs.org/w/index.php?diff=159978&oldid=159977 * BestCoder * (+5) 05:13:46 [[User:BestCoder]] https://esolangs.org/w/index.php?diff=159979&oldid=159978 * BestCoder * (-46) 05:20:09 -!- chiselfuse has quit (Remote host closed the connection). 05:21:08 -!- chiselfuse has joined. 05:27:27 [[Template:Start]] N https://esolangs.org/w/index.php?oldid=159980 * BestCoder * (+27) Created page with "{{{1}}} is an esolang where" 05:28:02 [[Esolang testing]] https://esolangs.org/w/index.php?diff=159981&oldid=149534 * BestCoder * (+10) 05:28:50 [[Esolang testing]] https://esolangs.org/w/index.php?diff=159982&oldid=159981 * BestCoder * (+2) 05:29:17 [[Template:Start]] https://esolangs.org/w/index.php?diff=159983&oldid=159980 * BestCoder * (+4) 05:29:43 [[Esolang testing]] https://esolangs.org/w/index.php?diff=159984&oldid=159982 * BestCoder * (+13) 05:41:37 [[Template:Start]] https://esolangs.org/w/index.php?diff=159985&oldid=159983 * BestCoder * (+8) 05:41:52 [[Template:Start]] https://esolangs.org/w/index.php?diff=159986&oldid=159985 * BestCoder * (-3) 05:42:15 [[Template:Start]] https://esolangs.org/w/index.php?diff=159987&oldid=159986 * BestCoder * (+14) 05:42:36 [[Esolang testing]] https://esolangs.org/w/index.php?diff=159988&oldid=159984 * BestCoder * (-15) 05:47:38 [[Two commands]] https://esolangs.org/w/index.php?diff=159989&oldid=128742 * BestCoder * (+38) 05:48:21 [[Category:Recursion]] N https://esolangs.org/w/index.php?oldid=159990 * BestCoder * (+22) Created page with "[[Category:Recursion]]" 05:53:39 [[Example]] https://esolangs.org/w/index.php?diff=159991&oldid=159966 * PkmnQ * (+28) Turning tarpits seems to be the more common name 05:56:49 [[Template:Notpossible]] N https://esolangs.org/w/index.php?oldid=159992 * BestCoder * (+44) Created page with ":''This esolang is impossible to implement''" 06:16:15 Well, I'm going to bed. Somebody else can clean this up. 06:45:49 [[Grass]] https://esolangs.org/w/index.php?diff=159993&oldid=120141 * Tpaefawzen * (+13) /* External resources */ DEAD LINK 06:49:11 -!- Sgeo has quit (Read error: Connection reset by peer). 06:51:07 [[Grass]] https://esolangs.org/w/index.php?diff=159994&oldid=159993 * Tpaefawzen * (+72) /* External resources */ implementation 07:06:25 -!- zzo38 has quit (Ping timeout: 248 seconds). 07:41:02 [[Special:Log/delete]] delete * Ais523 * deleted "[[Category:Instruction list pointer]]": undiscussed category 07:42:09 [[Special:Log/delete]] delete * Ais523 * deleted "[[Esolang testing]]": offtopic (not an esolang) 07:42:09 [[Special:Log/delete]] delete * Ais523 * deleted "[[Talk:Esolang testing]]": Deleted together with the associated page with reason: offtopic (not an esolang) 07:42:28 [[Special:Log/delete]] delete * Ais523 * deleted "[[Category:Recursion]]": undiscussed category 07:44:31 [[User talk:BestCoder]] https://esolangs.org/w/index.php?diff=159995&oldid=131302 * Ais523 * (+455) please stop creating categories without approval 07:45:32 [[Special:Log/delete]] delete * Ais523 * deleted "[[Template:Notpossible]]": this probably shouldn't be a hatnote; rather, the reasons should be discussed in the computational class section if they're interesting/nonobvious (see also [[Category:Uncomputable]]) 07:46:39 [[Special:Log/delete]] delete * Ais523 * deleted "[[Template:Start]]": not useful as a template; the page source would be more readable if you wrote that out manually, and most esolang pages won't want to start like that 08:02:04 -!- b_jonas has quit (Quit: leaving). 09:54:24 -!- ais523 has quit (Quit: quit). 10:14:47 [[Record]] https://esolangs.org/w/index.php?diff=159996&oldid=158866 * None1 * (+70) /* Commands */ 10:46:50 [[Record]] https://esolangs.org/w/index.php?diff=159997&oldid=159996 * None1 * (+1541) Add Python interpreter, implemented and TC proof 10:50:41 [[Record]] https://esolangs.org/w/index.php?diff=159998&oldid=159997 * None1 * (+112) /* Interpreter */ 10:51:35 [[Record]] https://esolangs.org/w/index.php?diff=159999&oldid=159998 * None1 * (+98) 10:53:40 [[Record]] https://esolangs.org/w/index.php?diff=160000&oldid=159999 * None1 * (+130) 10:55:34 [[Truth-machine]] https://esolangs.org/w/index.php?diff=160001&oldid=159881 * None1 * (+50) /* Realm */ 10:56:08 [[Record]] https://esolangs.org/w/index.php?diff=160002&oldid=160000 * None1 * (+0) /* Computational class */ Unary usually uses 0's rather than a's. 11:12:11 Hi 11:20:07 -!- V has quit (Ping timeout: 265 seconds). 11:40:17 [[]] https://esolangs.org/w/index.php?diff=160003&oldid=159975 * PrySigneToFry * (+416) 12:33:43 [[Grass]] https://esolangs.org/w/index.php?diff=160004&oldid=159994 * Tpaefawzen * (+3314) /* Examples */ 13:48:47 [[Untitled-Null]] https://esolangs.org/w/index.php?diff=160005&oldid=159917 * Hajunsheng * (+104) 13:59:48 [[Planes]] M https://esolangs.org/w/index.php?diff=160006&oldid=159963 * WhirlELW * (+366) added bold 14:01:03 [[Special:Log/upload]] upload * GreenThePear * uploaded "[[File:Rgbl hello world.png]]": Hello world program in rgbl 14:01:15 -!- wib_jonas has joined. 14:02:09 [[Planes]] M https://esolangs.org/w/index.php?diff=160008&oldid=160006 * WhirlELW * (+16) minor adjustment in behavior 14:05:43 [[Rgbl]] N https://esolangs.org/w/index.php?oldid=160009 * GreenThePear * (+6964) Page created 14:05:47 ais523: "the library takes a value and creates a type to represent it" => I don't understand how that would ever work in rust. I think I can believe you can do something like that in Haskell. Or you could do it in Rust but only to experiment with const generic parameters that aren't scoped, still have a compile time known value, but you want to do 14:05:47 something with them that rust's built-in const generic parameters don't yet support, eg. parameters of a user-defined aggregate type. 14:05:56 I also don't know what this should be called. 14:07:31 -!- Sgeo has joined. 14:11:37 https://www.youtube.com/watch?v=8taEllwQ2iE this might qualify for this channel 14:24:51 [[Language list]] https://esolangs.org/w/index.php?diff=160010&oldid=159953 * GreenThePear * (+11) Add rgbl 14:28:14 -!- wib_jonas has quit (Quit: Client closed). 14:30:38 [[User:GreenThePear]] https://esolangs.org/w/index.php?diff=160011&oldid=84452 * GreenThePear * (-460) Update for rgbl 16:33:53 -!- chiselfuse has quit (Remote host closed the connection). 16:34:19 -!- chiselfuse has joined. 17:16:47 [[Planes]] M https://esolangs.org/w/index.php?diff=160012&oldid=160008 * WhirlELW * (-3) 17:22:02 -!- amby has joined. 17:50:46 [[User talk:Ais523]] https://esolangs.org/w/index.php?diff=160013&oldid=158849 * Aadenboy * (+348) /* scrapped template */ new section 17:51:51 [[User:Aadenboy/wikipiss]] https://esolangs.org/w/index.php?diff=160014&oldid=159555 * Aadenboy * (+383) 17:56:38 -!- zzo38 has joined. 18:24:26 [[Triolang]] https://esolangs.org/w/index.php?diff=160015&oldid=159711 * BestCoder * (+28) 18:36:16 [[Nested one input functions]] https://esolangs.org/w/index.php?diff=160016&oldid=135898 * BestCoder * (+51) 18:43:34 [[Infinid]] N https://esolangs.org/w/index.php?oldid=160017 * BestCoder * (+18) Redirected page to [[D]] 19:09:03 -!- b_jonas has joined. 19:50:56 [[Special:Log/delete]] delete * Ais523 * deleted "[[Template:Minpre]]": unused template, author requested deletion 20:22:52 [[Planes]] M https://esolangs.org/w/index.php?diff=160018&oldid=160012 * WhirlELW * (+24) edited $, removed ! and added = 20:26:24 [[Planes]] M https://esolangs.org/w/index.php?diff=160019&oldid=160018 * WhirlELW * (+77) 20:32:10 [[Planes]] M https://esolangs.org/w/index.php?diff=160020&oldid=160019 * WhirlELW * (+66) added WIP message 20:32:34 [[Planes]] M https://esolangs.org/w/index.php?diff=160021&oldid=160020 * WhirlELW * (+0) moved wip message up 20:33:10 [[Planes]] https://esolangs.org/w/index.php?diff=160022&oldid=160021 * WhirlELW * (+0) moved wip message to the instruction set section 20:36:21 [[Planes]] M https://esolangs.org/w/index.php?diff=160023&oldid=160022 * WhirlELW * (-41) fixed inaccuracy in behavior section 21:12:19 [[Works in progress]] M https://esolangs.org/w/index.php?diff=160024&oldid=156082 * WhirlELW * (+13) added planes 21:24:04 [[Planes]] https://esolangs.org/w/index.php?diff=160025&oldid=160023 * WhirlELW * (+145) edited instruction set 21:36:22 [[Planes]] https://esolangs.org/w/index.php?diff=160026&oldid=160025 * WhirlELW * (+637) added 99 bottles of beer program 22:03:47 [[Planes]] M https://esolangs.org/w/index.php?diff=160027&oldid=160026 * WhirlELW * (-66) removed wip message as the instruction set wont change anymore 22:32:00 [[User:Shazun bhasfu]] N https://esolangs.org/w/index.php?oldid=160028 * Shazun bhasfu * (+137) userpage? 22:50:09 [[User talk:I am islptng]] https://esolangs.org/w/index.php?diff=160029&oldid=159853 * Hotcrystal0 * (+498) /* New esolang idea */ new section 22:55:49 -!- ais523 has joined. 22:57:23 "the library takes a value and creates a type to represent it" => I don't understand how that would ever work in rust ← create a global variable, store the value in the global variable, create a type (it doesn't matter what the type actually stores so you can use a ZST), have the deref implementation on the type read from the global variable, use lifetime trickery + runtime checks to ensure that the variable is always initialised when you try to use it and 22:57:24 never tries to store two values at once 22:57:35 (the last requirement means that this doesn't work properly in recursive code, but I can live with that) 22:57:56 and by "doesn't work properly" I mean a deterministic panic, not UB 23:15:11 [[DisFuck]] M https://esolangs.org/w/index.php?diff=160030&oldid=159430 * Tpaefawzen * (+5) /* Overview */ note of braces resolving 23:40:58 -!- Lord_of_Life_ has joined. 23:41:53 -!- Lord_of_Life has quit (Ping timeout: 268 seconds). 23:42:20 -!- Lord_of_Life_ has changed nick to Lord_of_Life. 23:46:02 -!- Noisytoot has quit (Excess Flood). 23:48:45 -!- Noisytoot has joined.