Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
zeroexcuses
@zeroexcuses
True, maybe I should specify it as Haskell98 w/o extensions -- that, I think, is still straight forward.
Fabio Labella
@SystemFw
yeah, I agree with that, but that language essentially doesn't exist in practice, ~every single library on earth uses various extensions
zeroexcuses
@zeroexcuses

Wait, so is Scala3 fully dependently typed? i.e. can we have type signatures f the form

concat(a: Vec of length M, b: Vec of length N) -> Vec of length (M + N)

?

Fabio Labella
@SystemFw
scala 3 is not fully dependently typed
although the type signature you have used as an example doesn't required full dependent types
Scala uses the term "dependent typing" for a feature which, although it shows a certain degree of "dependence", isn't full dependent types a la Idris or Agda
zeroexcuses
@zeroexcuses
in terms of lambda cube, can we have types that depend on values ? i.e. n: Int, v: Vec of length n
Martijn
@martijnhoekstra:matrix.org
[m]
scala 3 has the same path dependent types as scala 2: if you have a trait Foo { type X }, and a value val foo: Foo (but not var foo or def foo), then you can talk about the type foo.X
Fabio Labella
@SystemFw
@zeroexcuses not directly, so Scala is not fully dependent
an easier definition is to consider where the "type arrow" is the same as the "value arrow"
in Scala it's not
the type arrow in Scala is [A, B], the value arrow is =>
in Idris they are the same
Rich
@Rich2
What do people think of how Idris 2 is shaping up?
zeroexcuses
@zeroexcuses
I really hope Idris succeeds, but imho, dependently typed languages suffer the problem that you need really really really good IDE integration to fill in types.
Rob Norris
@tpolecat
This message was deleted
bblfish
@bblfish:matrix.org
[m]
I was just looking at cats.Show. The documentation does not provide very good reason to use it. I wonder if I have found one.
I have written co-operating-systems/Reactive-SoLiD#13 that produces datastructues like ListMap, Long a Dictionary and a few others, and I would like to have specify a way to serialise the results for HTTP Signature. This needs to be done in a precise way. Is this the right place to use Show?
Ethan
@esuntag:matrix.org
[m]
bblfish: You can think of Show largely as a better version of toString, ensuring that there is a sensible String representation of the object. I'd be hesitant to use it outside of debugging and logging contexts. If you need to serialize, then you probably want some sort of Encoder typeclass
bblfish
@bblfish:matrix.org
[m]
Ah good to know. Is theree a good one I should use?
Ethan
@esuntag:matrix.org
[m]
If you're serializing to json, you probably want to look at circe
I believe scodec is supposed to be good for binary formats, although I haven't used it myself
bblfish
@bblfish:matrix.org
[m]
I serialising to HTTP headers strings. But it has to be very precise so that it can be signed. https://tools.ietf.org/html/draft-ietf-httpbis-message-signatures-03
It should also be flexible so that I can provide serialisation for akka http header fields, or for other frameworks if needed. (In case they don't provide the right output).
(I should be using circe at some point later for parsing JSON. Actually I want to write a streaming non-blocking JSON-LD parser at some point)
Ethan
@esuntag:matrix.org
[m]
I'm not sure if there is some specific library to help with the headers (perhaps an HTTP4S component?), although if you're already looking at Show you can just throw together your own HttpEncoder typeclass with similar functionality pretty easily
bblfish
@bblfish:matrix.org
[m]
ok. I'll study how it works a bit more carefully.
Ethan
@esuntag:matrix.org
[m]
"streaming non-blocking json parser" sounds exactly like what fs2+circe gives you out of the box. I'm not sure how much complexity the LD adds
bblfish
@bblfish:matrix.org
[m]
probably not that much. IT would be an extra layer one would have to build on top I guess, to re-interpret the JSON in terms of RDF Quads.
It hope it will turn out to be that easy :-)
Rob Norris
@tpolecat
Show is not very useful. It can keep you from inadvertently calling toString on things that have no toString, but that's it. In our codebase toString is always and only for debugging and Show always does the same thing as toString. If you need a domain-specific stringability I recommend defining your own typeclass for it.
bblfish
@bblfish:matrix.org
[m]
Following the pattern of cats.Show I wrote up this in Scala3 https://github.com/co-operating-systems/Reactive-SoLiD/blob/master/src/main/scala/run/cosy/http/headers/Rfc8941.scala#L135 . One could make it more efficient by using Rope or something like that, as scalaz does. But I can get to that later.
zeroexcuses
@zeroexcuses
news
Ross A. Baker
@rossabaker
As I recall, the constant factors on Cord or Rope are ghastly, and you had to be assembling a lot before it was better than the dreaded String concat. And then at that scale, you'd be better off with a StringBuilder if you could hide the mutation. I tried to use it a few times, and it's clever, but I could never find a place that it was the best option.
zeroexcuses
@zeroexcuses
besides, 'jvm', what are the biggest differences of OCaml vsScala ?
bblfish
@bblfish:matrix.org
[m]
Is there a typesafe ascii string type? For formatting http headers?
Michael Ahlers
@michaelahlers
@bblfish, if there isn’t already there can be. Check out https://github.com/fthomas/refined.
bblfish
@bblfish:matrix.org
[m]
Thanks @michaelahlers I had come across that but could not remember where. Are they going to have trouble moving to Scala3 given the use of macros?
Michael Ahlers
@michaelahlers
I can’t answer that, and—while not a long-term solution—Refined is cross-compiled against 2.13, which Scala 3 can depend on. See section “The Scala 2.13 TASTy Reader” from https://scalacenter.github.io/scala-3-migration-guide/docs/general/compatibility.html.
Oops, I have that reference backwards. 😅
bblfish
@bblfish:matrix.org
[m]
yes. It looks very interesting.
Michael Ahlers
@michaelahlers
The section right before it.
bblfish
@bblfish:matrix.org
[m]
I know. My own library banana-rdf is having trouble moving to Scala3 because of the removal of type projections. https://github.com/lampepfl/dotty-feature-requests/issues/14#issuecomment-815928271
bblfish
@bblfish:matrix.org
[m]
Though that covers a lot more, not just strings...
Adam Rosien
@arosien
@bblfish:matrix.org there's https://github.com/typelevel/case-insensitive, which i think might be useful for headers, since @rossabaker wrote it
but i can't remember the RFC anymore
Ross A. Baker
@rossabaker
case-insensitive was written for http4s, and used in its modeled headers, but can represent characters that are illegal in headers.
bblfish
@bblfish:matrix.org
[m]
Ah yes, I saw that one be used by http4s :-)
Ross A. Baker
@rossabaker
I've thought about tightening those headers down to make illegal states unrepresentable, but haven't figured it out without making the library unusable.
Refined is probably the closest.