Perl 6 - the future is here, just unevenly distributed

IRC log for #6macros, 2015-10-06

| Channels | #6macros index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
01:45 vendethiel joined #6macros
06:31 FROGGS joined #6macros
06:35 Ven joined #6macros
08:03 Ven joined #6macros
08:37 Ven joined #6macros
09:47 Ven joined #6macros
09:57 Ven joined #6macros
11:11 Ven joined #6macros
13:22 Ven joined #6macros
16:14 Ven joined #6macros
17:52 FROGGS joined #6macros
18:55 vendethiel joined #6macros
18:59 masak vendethiel: how come dependently typed languages are so "stiff"? I'm trying to understand this.
18:59 vendethiel I'll need a (n informal) definition of "stiff" :P
19:00 masak for example: Idris. requires things to be total.
19:00 vendethiel no. use %partial
19:00 vendethiel :P
19:00 masak huh, ok
19:00 masak I think my point still stands, though.
19:00 vendethiel well
19:00 vendethiel you can't offer the same guarantees otherwise
19:00 masak all dep-typed languages I've seen seem to also be weird in one way or another
19:00 vendethiel well, say, type inference
19:00 masak I suspected the answer would be that
19:00 vendethiel it's undecidable in dep-typed langs
19:01 vendethiel at least, that's what it seems "right now" ;-)
19:01 masak basically because the type level is now basically Turing complete, right?
19:01 vendethiel yeah
19:01 vendethiel well, it also is in haskell given type families.. :)
19:01 vendethiel of course, that's my "practical" PoV, I don't know much about the theory
19:01 vendethiel I need to go back to learning about TT, I've been on a "hiatus" for a while
19:02 vendethiel (and I've had great tons of fun!)
19:02 masak :D
19:03 masak I'm just thinking -- how "normal" could you make a language, and still have dependent types?
19:03 * vendethiel turns his nose at Perl 6
19:03 vendethiel without the joke now --
19:03 masak like, something like 007. nothing fancy at all. just an Algoloid.
19:03 vendethiel the worst offender is probably Shen :P
19:03 vendethiel Idris has a {} syntax (like haskell), AFAI{K,R}
19:04 vendethiel ... not a real argument
19:11 masak I understand that many of these live in the FP world, where the baseline is Haskell and weirdness isn't so scary
19:11 masak I'm just wondering how much one could make a dep-typed language "blend in"
19:11 masak TypeScript blends in amazingly as a structurally typed language. Ocaml somewhat less so.
19:13 vendethiel ..I have a feeling these people don't want to blend in, though.
19:13 vendethiel "success at all cost", yada yada yada
19:13 masak well, I do. that's what I'm saying.
19:13 masak I would be willing to write a toy language to find out :)
19:13 masak another question: are there any obvious blockers for Perl 6 to be dependently typed, or is it more of a "no, it's just not possible to get there from here" kind of thing?
19:23 vendethiel mmh
19:24 vendethiel well, the focus definitely isn't there, to start with
19:24 * vendethiel goes to talk a bit more with the family, brb&
19:26 vendethiel no, let's not instead
19:27 * masak checks whether dependent types are mentioned in TaPL
19:27 masak they are; but not until on pages 462..466
19:27 masak that's near the end of the book
19:32 vendethiel also
19:32 vendethiel one BIG, BIG issue is the mixin "instanciation" time
19:32 vendethiel s/c/s/
19:33 vendethiel or t. anyway...
19:59 vendethiel if you expected me to follow up:
20:00 vendethiel I'd really, really, really, really, see as a "big thing" to have a "constrainable".. kinda thing.
20:00 vendethiel somewhat like "template<typename T> using foo = some_complex<T>::expr;"
20:00 vendethiel subset NotEmptyList[T] of List[T] where .elems;
20:00 vendethiel i.e.
20:46 masak joined #6macros
21:04 masak interesting
21:06 masak especially interesting since List[T] is a monoid, and has an "empty" value ([]), whereas NotEmptyList[T] isn't, and doesn't
21:06 masak so there kind of isn't a default
21:06 vendethiel there's none, for sure
21:06 vendethiel that's not an issue though. it's just a type.
21:07 vendethiel doesn't have to be instantiable :)
21:07 masak then I think I misunderstood what you meant the BIG, BIG issue is :)
21:07 vendethiel the big issue that
21:07 vendethiel instantiation time is not compile time
21:08 vendethiel and I can't just alias stuff up with some kind of "using" construct, only with subset, which doesn't take type params
21:09 masak oh, are you talking about a big issue with Perl 6 in particular?
21:09 vendethiel yes
21:09 vendethiel isn't that what you asked?
21:09 masak among other things, yes :)
21:10 masak so, what would it mean for instantiation time to be compile time? do you have an example?
21:10 vendethiel role Foo[::T]{ constant T a  .= new }
21:12 masak $a, right?
21:12 masak oh wait, it's a constant. nvm
21:13 masak just tried it on #perl6
21:13 masak trying to understand why exactly it fails the way it does
21:15 masak hm, because it's trying to run T.new without the role having been used somewhere.
21:15 masak it's like it's taking it too literally somehow
21:15 vendethiel yeah.
21:15 vendethiel it's because constant is compile-time
21:15 vendethiel not instantiation time
21:15 masak ah, that's what you mean by "instantiation"
21:15 vendethiel yes
21:15 vendethiel role instantiation
21:15 masak got it
21:16 masak right
21:17 vendethiel yeah.
21:17 vendethiel :(
21:17 vendethiel that + not being able to access subsets defined inside of a role are my biggest gripe
21:23 masak ok, so. here and now. let's draw up a really small Algol-like language with types, typed variables, and dependent types.
21:23 masak does it need classes, or are roles enough?
21:24 masak is the list-of-length-N example the "hello world" of dependently typed languages? is that the level to aim for at first?
21:24 vendethiel here and now? It's almost midnight, and I need to wake up at 6am
21:25 vendethiel so it's not really the best time for that :-)
21:25 vendethiel roles and classes ought to be merged
21:25 masak thought so
21:25 masak yeah, I don't have time either to design a language right now
21:25 vendethiel ;-)
21:25 masak we can both think about it until tomorrow, then
21:26 vendethiel and by think, you mean sleep on it :P. Good night!
21:26 masak 'night
21:28 * masak looks at http://www.idris-lang.org/example/

| Channels | #6macros index | Today | | Search | Google Search | Plain-Text | summary