<discocaml>
<lukstafi> Is may understanding of modular explicits correct? I can already write `let f (type a b c d) (module M : MT with type a = a and b = b and c = c and d = d) (x : M.u) : unit = ...` -- and with modular explicits I'll be able to drop the bloat of abstracting the `a b c d` abstract types.
<discocaml>
<lukstafi> Note: that's where `u` is not itself abstract, but defined e.g. indirectly to depend on `a b c d`.
<discocaml>
<lukstafi> Or, will I still need the bloat even with explicits?
<discocaml>
<lukstafi> My thinking is that with explicits I can write: `let f : (module M : MT) -> M.u -> unit = fun (module M) x -> ...`
<discocaml>
<octachron> The two are not strictly equivalent: the first function is not path dependent, thus can be used with (dynamic) first-class module, whereas the second is path dependent and can only take (static) module paths as its first argument.
<discocaml>
<._null._> Recursivity is the default for types, shadowing is the default for values. Conversely, recursivity is opt-in for values and opt-out for types
<discocaml>
<softwaresirppi> how do you optout?
<discocaml>
<softwaresirppi> and why is this made this way
<discocaml>
<softwaresirppi> OHHH thats a good reason for opt-in rec
<discocaml>
<softwaresirppi> i probably wont be doing these to types
<discocaml>
<softwaresirppi> is that what youre saying?
ds-ac has joined #ocaml
<discocaml>
<._null._> let rec is also the more complex notion, so it makes sense to have it heavier syntactically. For types, the difference is less pronounced (and you very frequently want them to be recursive)
<discocaml>
<softwaresirppi> doenst work in utop?
<discocaml>
<gooby_clown> I mean sure yeah, I didn't think of it that way but it's not wrong
<discocaml>
<softwaresirppi> what do you think offf
<discocaml>
<softwaresirppi> enlighten mee
semarie has quit [Quit: connection reset by purr]
<discocaml>
<gooby_clown> It's just that most types you write happen to be recursive
<discocaml>
<gooby_clown> Especially with compilers which is a popular use-case for this language
<discocaml>
<gooby_clown> Under the assumption that syntax should cater to likely use-cases, the recursive syntax for types should be lighter
<discocaml>
<gooby_clown> Whereas, in OCaml anyways, regular definitions should *not* be recursive in most instances, usually it's limited to either the top function definition, or an auxiliary inside of it (usually like `let rec go`)
<discocaml>
<gooby_clown> In Haskell since it's lazy, things like `let xs = 1 : xs` are more common
<discocaml>
<softwaresirppi> alright
<discocaml>
<softwaresirppi> satisfiable
<discocaml>
<softwaresirppi> anyways what doing gooby
<discocaml>
<softwaresirppi> guyss
<discocaml>
<softwaresirppi> if `type numbers = None | (::) of int * numbers` works, then why `(::) 1 [2; 3]` doesnt work?
<discocaml>
<softwaresirppi> also `type a = A | B | [] | ()` works BUT `type b = {} | 0` doesnt work
<discocaml>
<softwaresirppi> isnt `[]` and `()` just a value? it gets accepted in the place of a constructor?
Anarchos has joined #ocaml
<discocaml>
<._null._> 1. `(::) (1, [2; 3])`
<discocaml>
<._null._> 2. `()` and `[]` are constructor operators (they're the only ones with `(::)`), so no other ones are accepted
<discocaml>
<leviroth> People say this but I think it depends on the type of work that you do, and in particular it's less true outside of academic contexts. Like:
<discocaml>
<leviroth> - The binary trees that you learn about in your data structures and algorithms class are recursive.
<discocaml>
<leviroth> - The syntax trees that you define in your PL research are recursive.
<discocaml>
<leviroth> - The `list` type that you see demonstrated in OCaml 101 is recursive.
<discocaml>
<leviroth> But personally I'd guess that most types I write are boring non-recursive record types that track the state of some component of a system, or boring non-recursive variant types that define choices for the user of some API.
<discocaml>
<lukstafi> For example I tend to have an auxiliary `let rec loop ...`
<dh`>
you're concerned about inconsistent syntax and it's "let rec" that bothers you?
Anarchos has quit [Quit: Vision[]: i've been blurred!]
<dh`>
leviroth: I'd agree, most types that aren't containers or abstract syntax are flat
<dh`>
however, both containers and abstract syntax are common, abstract syntax particularly so in compiler-flavored languages
<discocaml>
<._null._> What inconsistency are you thinking about ?
pi3ce_ has joined #ocaml
pi3ce has quit [Read error: Connection reset by peer]
<dh`>
well for example the fact that functions, constructors, types, and functors all have different incompatible argument syntax
<dh`>
(and for no real reason, unlike let rec which has semantics)
<discocaml>
<._null._> Functions vs constructors has good reasons, I think functors has a technical reason but I can't recall, and I admit that types only have historical reasons
<dh`>
constructors are semantically different, but there's no reason for them to be syntactically different
<dh`>
there's a bunch of fraught history with multiple functor arguments, but the point isn't how we got here, it's that where we are has some shortcomings
<discocaml>
<._null._> Application by juxtaposition is to allow partial applications; it's better to make partial application impossible for beginners' sake
<dh`>
I don't agree, I think not being able to partially apply a constructor is a bug
<dh`>
(and I'm not sure how this affects beginners in particular)
<discocaml>
<._null._> I've has this discussion here a few days ago, but it's really not a bug; partially applied constructors don't make sense at all
<dh`>
as in, beginners getting confused because they get wild types out if they forget arguments happens with functions, making it not happen with constructors doesn't seem like it makes much difference
<dh`>
tell that to all the (fun x y -> FOO (thingy, x, y)) in my code
<dh`>
it comes up, it's easy to work around but the workaround is unsightly, and there's no reason it needs to be that way
<discocaml>
<._null._> If you have the log, it was 5 days ago
<discocaml>
<Kali> wasn't that for coq specifically though
<dh`>
even if I don't, there's a public logger
<discocaml>
<._null._> It's even truer for Coq, but the meaning part applies in any context
<discocaml>
<._null._> The crux is that constructors are not functions
<discocaml>
<Kali> sure, but why shouldn't they be syntactically applied like one when this is an extremely common pattern
Everything has joined #ocaml
<dh`>
from the scroll it's something about universe polymorphism in coq
<dh`>
also, I don't agree that constructors aren't functions; FOO in a type t = FOO of int is a mapping between ints and ts
<dh`>
so they're certainly math functions and program functions when they aren't math functions are whatever you say they are
<dh`>
so nu
<discocaml>
<._null._> By function, I mean "things that compile to assembly functions", and constructors are not. You can't call constructors, they have no existence of their own
<discocaml>
<._null._> I wouldn't mind some sugar for `foo = fun x y -> FOO (x, y)`, but the distinction should still exist
<dh`>
oh, I don't care if the compiler internals treat constructors differently, there's lots of reasons that's desirable
<dh`>
there is no good reason to have them be different from functions in the concrete syntax
<dh`>
(and re coq, once you're dealing with universe polymorphism at all you're already in a bad world and should consider your life choices)
<discocaml>
<._null._> "When you're dealing with parametric polymorphism at all you're already in a bad world and should consider your life choices" -- an old C developer I guess
<dh`>
and they do generate _some_ assembly code in the general case, there's at least one instruction that writes a tag somewhere
<dh`>
eh? that is an unreasonable leap
<discocaml>
<._null._> There is code which is actually internal details, but no *function* that can be called. It's pure data management
<dh`>
but I am in fact an old C coder so I'd like to hash this out
<dh`>
except I have to go, so later/tomorrow?
<discocaml>
<._null._> Universe polymorphism is the next level of parametric polymorphism in a dependent language, they behave the same
<dh`>
yes, I know
<dh`>
it's just a horror show in coq
<discocaml>
<._null._> (That's true, but unrelated)
<dh`>
it's not unrelated, it's why I said you're in a bad world