Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    Henry Story
    @bblfish
    Will go back from reading on law to DL and then back to Scala
    Gavin Bisesi
    @Daenyth

    I think it's becoming clearer to me what things look like.

    Let a Record be an unordered product type where each product element is tagged with a known name.

    Transformations could be declared as first-class objects (a la free applicative models of algebra construction)

    Transformations declare the manner in which they transform something immediately. In contrast to eg: fmap on an Option[A] taking A => B, a Transformation encodes a profunctor-ish shaped (some connection to lenses here I'm certain) transformation either on specific keys, all keys, any keys having some sort of deterministic property, all product fields of a certain type, etc, and declare exactly how the resulting Record is changed - either by removing or adding key-type fields

    Transformations can be polymorphic, for example:

    input: r with { "password": String }
    output: r with { "password": CryptedString }

    the result { "password": CryptedString } splices onto whatever r is given as an input. Because the field "password" is the same name, the new type replaces the old one

    Gavin Bisesi
    @Daenyth
    There's some definite relation to purescript's row types, but polymorphic row types are only type-level constructs. We need a vocabulary of reified transformations to talk about an algebra of transformation composition
    And such transformations could compose in the same manner as normal functions

    Transformations would exist somewhere between value and type level. They would define a value-level algorithm to implement their type-level changes.

    New nominal or structural types could be declared as applying some Transformation to a given type

    so for example: a "sparse PATCH" model for a CRUD http api might define a Patch transformation something like:
    enum Patch a = Update a | Remove | Ignore
    { r | foreach k:t in r -> k: Patch t }
    Gavin Bisesi
    @Daenyth
    hmm so some transformations might apply only at the type level - that one has no value equivalent. We could apply that transform to a type data User = { name: String, age: Int } like:
    type UserPatch = Patch(User)
    // data UserPatch = { name: Patch String, age: Patch Int }
    anyway heading out for the day
    Ryan Wisnesky
    @wisnesky
    have you seen the work on algebraic property graphs? it is based on mediating between graph models that are based on algebraic datatypes. a transformation of a schema is a 'signature morphism', i.e., Functor like thing, combining type and value level operations at once
    Henry Story
    @bblfish
    in his 2003 thesis Access control for the web via proof-carrying authorization L.Bauer uses PCA (proof-carrying authorization) logic, a higher order logic in order for clients to send proofs that they are authorized to access a resource. I guess my main question is: how close can we get to that with RDF?
    Joshua Shinavier
    @joshsh
    @wisnesky thx
    will cite both in the Dagstuhl paper
    Joshua Shinavier
    @joshsh
    @Daenyth I would definitely check out CQL (and APG, too). You can probably get pretty far with the simple mapping language Ryan describes in the paper (https://arxiv.org/abs/1909.04881, section 3.2.3). FYI, Ryan and I are getting ready to do some more work together around transformations specifically. Might be a chance for some interesting discussions in this channel.
    Gavin Bisesi
    @Daenyth
    @wisnesky That sounds really related to what I've been thinking about
    Ryan Wisnesky
    @wisnesky
    the APG stuff? It's implemented in CQL if you want to play with it. Uber's version will get open-sourced eventually too.
    Henry Story
    @bblfish
    I found a very interesting article from 2003 that gives an overview of how Databases fit in the larger information System Design space. IS=DBS+Interaction: Towards Principles of Information System Design. It looks at OO, Agent based systems, coalgebras, Speech acts, Categories as and Abstract state machines, etc... It's an overview, but it is very useful.
    Henry Story
    @bblfish
    Screen Shot 2020-03-21 at 10.31.06.png
    Henry Story
    @bblfish
    actually the article is from 2000 (it was published online 2003). So the authors were really at the bleeding edge.
    Henry Story
    @bblfish
    I have come across some really interesting work that is helping me understand type theory better.
    I was looking around for how speech acts apply to logic and found that Martin-Löf had given a couple of talks on the subject in 2018. Martin-Löf's type theory is what led to Homotopy Type Theory.
    The talk was nowhere to be found on the internet but has been transcribed by Ansten Klev who is one of the coauthors of the book "Immanent Reasoning or Equality in Action".
    That has helped answer a lot of questions I had coming from Philosophical Logic stemming from Frege and Russel. The book really helps point at the differences, but from a Dialogical point of view. CTT seen from a dialogical lens!
    Henry Story
    @bblfish
    Their claim is that "Logic has its roots in Ethics"
    Henry Story
    @bblfish
    Now it would be interesting to find the relation to Cats. I guess it comes from most connectives arising out of adjunctions, relation two categories.
    Henry Story
    @bblfish
    I found Per Martin-Löf's talk "Logic and Ethics" https://twitter.com/bblfish/status/1243936439961870337
    Henry Story
    @bblfish
    This is quite tangential to this group but could be of interest co-immunology and the web. On the other hand who knows. There may be relations to cats that could be usefully explored. I don't know them.
    Henry Story
    @bblfish
    It looks like a large number of people are on Zulip chat to discuss category theory. https://twitter.com/_julesh_/status/1242141831057616896
    It allows for a number of channels and one could then open a Web Cats channel there.
    Henry Story
    @bblfish
    I asked a question about that here to see what they think https://categorytheory.zulipchat.com/#narrow/stream/229111-general/topic/Web.20Cats
    Ryan Wisnesky
    @wisnesky
    oh this is a w3c group and their zulip thing can't be because it's closed?
    Henry Story
    @bblfish
    well we have not yet become a w3c Community group, but thas was the idea. Not sure how much value that brings.
    In any case that group is closed, which would not fit. Will need to find out if that is temporary.
    Henry Story
    @bblfish
    I managed to work out how co-constructive logic works (the Popperian logic of falsification, and dual to constructive logic loved by FP programmers), illustrating it with a simple example explaining co-implication. https://math.stackexchange.com/questions/3621660/examples-of-co-implication-a-k-a-co-exponential/3624965#3624965
    Ryan Wisnesky
    @wisnesky
    co-exponential is a new phrase to me
    Henry Story
    @bblfish
    The first answer on that 6 year old StackExchange answer forgets to transform the product into a co-product.
    Henry Story
    @bblfish
    Now that I have a good example of how co-exponentials work, I wonder if dependent probabilities are not a type of co-exponential.
    Henry Story
    @bblfish
    There seems to be disagreement on what the word co-exponential refers to. (Someone answered my StackExchange answer to the question you linked to above)
    Henry Story
    @bblfish
    A very interesting thesis
    "Model and Proof Theory of Constructive ALC
    Constructive Description Logics"
    https://twitter.com/bblfish/status/1267766917546336258
    This has relation between constructive logic and Curry-Howard and OWL has intrigued me for a while. One one side programming #Scala we have something build on Constructive Logic, on the other hand OWL and RDF on first order logic.
    Henry Story
    @bblfish
    There is more happening on the Zulipchat channel than here, so it seems like it may be better to continue the conversation there. I have opened an Web Cats channel in the Applied Category Stream.
    Henry Story
    @bblfish
    I think one needs an invite for that channel. IT changes every so often. There is the current one https://categorytheory.zulipchat.com/join/crexj49uvyghzyiwjvezf1hl/
    Henry Story
    @bblfish
    The archive of web-cats discussion on Zulip is now publicly available here https://mattecapu.github.io/ct-zulip-archive/stream/229156-practice:-applied-ct/topic/web.20cats.html
    For those who want full access to the firehose of mathematical thinking you can look here: https://mattecapu.github.io/ct-zulip-archive/ :-)
    GlobalYou
    @globalyou:matrix.org
    [m]
    Hello everyone
    can anyone guid me how to activate my web3 wallet to connect with L2 wallet
    ?
    bblfish
    @bblfish:matrix.org
    [m]
    This is not a channel about wallets :-)
    B
    @globalyou:matrix.org
    [m]
    Hello everone