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

Powered by Cro and the Raku® Programming Language.

Please report any issues / comments / feature requests as an issue on App::Raku::Log.

Thank you!