Re: [racket-users] Moving a Rust/Haskell abstract algebra library to Racket?
On Fri, Jan 22, 2021 at 12:56 AM Hendrik Boom wrote: > [...] > > You might also want to look at the implementations of category theory in Agda. > Agda is a language which unifies execution and correctness proof to some > extent. > > Not that you want to implement catagory theory, but category theory is a > form of algebra, and you may find some useful ideas about syntax and > semantics there. > > I attended an online seminar about this recently, but I haven't been > able to find the details again. The following links seem to refer to the > same project. (I found them looking for > category theory in agda Thanks Hendrik -- I had forgotten that Agda (and Idris, Coq, Lean) are also good sources of inspiration in this general area. Stu -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAG%2BkMrGTrbQuoFuYq%2BGWQKch0VZukQyuc6ngR0jhAwsxvidXVw%40mail.gmail.com.
Re: [racket-users] Unsafe structs
On Wed, Jan 20, 2021 at 5:16 PM Dominik Pantůček wrote: > > Hi Sam, > > I went through all my notes and prepared minimal (sometimes) working > examples for most of the issues I mentioned. Let's go through it one by > one. I assume that some of the complications I encountered were because > my lack of experience with Typed Racket. I hope some of these examples > will be useful anyway. > > All the examples are in a git repository on Gitlab [1]. This is great, thanks! I've opened several issues for fixing some of these problems. > >> * Higher-order procedures and polymorphic functions in all imaginable > >> combinations. That was a total disaster. Yes, the documentation clearly > >> states that - but typing any code using these is like trying to break a > >> badly designed cipher. Irregularities here and there. Sometimes simple > >> `inst' was enough. Sometimes casting both the function and the arguments > >> was necessary. The biggest trouble is that the error messages are very > >> cryptic and sometimes even do not point to the offending construct but > >> only the module file. I will provide MWE to show this if someone wants > >> to look into it. > > > > An example would be great here. In general you should only need one > > use of `inst` in any of these cases, and you shouldn't ever need a > > `cast`. > > Directory "polymorph". In my use-case, there is a lot of structured > S-expression data in the format: > > (define tagged-data-example > '(data-2D > ((B B B B) > (B B B > > 9 steps of typing the procedure to calculate the maximum length of the > 2D matrix are in this directory. All the errors are documented there. > Yes, many of the intermediate constructs are wrong. The error in > polymorph4.rkt shows the biggest problem I've seen so far. As a separate > example, it is pretty easy to fix - but finding the source of the > problem in a bigger module was not easy at all. Basically I ended up > bi-partitioning the whole source code with procedure granularity and > once I found the offending procedure a linear trial-and-error approach > was the only option that allowed me to find the offending expression. > > Yes, the final polymorph9.rkt contains the approach that I actually used > for resolving the issue. Yikes, this is pretty terrible. Here's a nice simple version that works, though: (define (typed-extract-data (tagged-data : (Pairof Symbol (Listof (Listof (Listof Symbol)) : Number (define data (car (cdr tagged-data))) (define lengths (map (inst length Symbol) data)) 1) What's going on here is: 1. The type for `cadr` is not quite smart enough -- if it knows that you have an at-least two element list, then it will produce the second element type. Otherwise, if you have a (Listof T), it produces T. But if you have a pair of a T and (Listof S), that ends up with (Union S T). 2. I think there's a missing `syntax/loc` in the implementation of `cast`, which resulted in the bad error message you saw. I also think you're jumping too quickly to use `cast` -- before you do that, you should try `ann`, for example, with the types of `length` that you tried, which would have accomplished the same thing and doesn't hide type errors or impose runtime costs. > The actual problem I was referring to here is nicely shown in the > "union" directory and it is about typing hash-union procedure. > > I do not know what solution should be considered correct if there were > multiple differently-typed hash-tables in the same module. The explicit > type information in require/typed is definitely not a good idea - but I > found no better way. Well, first we should make `racket/hash`'s exports work automatically. But absent that, there are a few things going on here: First, using `Any` is forgetting information, which is why the version with `Any` everywhere produced an unsatisfactory result. In general, one misconception I see regularly with Typed Racket users is using a general type (such as `Any`) and then expecting Typed Racket to specialize it when it's used. If you want that, you'd need to write a polymorphic type, like this: (hash-union (All (a b) (-> (Immutable-HashTable a b) (Immutable-HashTable a b) (Immutable-HashTable a b) Unfortunately, while this is the type you want, it can't work here because contracts for hashes are limited in various ways. There are a couple options to work around that. 1. Use `unsafe-require/typed` from `typed/racket/unsafe`. This works with the type as written, but obviously if you make a mistake things can go poorly. 2. Use a more restrictive type, such as `Any` or `Symbol` for the keys. > >> * Classes: My notes say "". Which roughly says it > >> all. Although I managed to back down to only using bitmap% class, > >> properly typing all procedures using it was a nightmare. By properly I > >> mean "it compiles and runs". > > > > More detail here would be
Re: [racket-users] Moving a Rust/Haskell abstract algebra library to Racket?
On Wed, Jan 20, 2021 at 08:06:45PM -0800, Stuart Hungerford wrote: > On Thursday, 21 January 2021 at 10:22:45 UTC+11 Jens Axel Søgaard wrote: > > Den ons. 20. jan. 2021 kl. 08.43 skrev Stuart Hungerford < > > stuart.h...@gmail.com>: > > > >> On Wednesday, 20 January 2021 at 12:34:59 UTC+11 Robby Findler wrote: > >> > >> I'm no expert on algebras, but I think the way to work on this is not to > >>> think "what Racket constructs are close that I might coopt to express > >>> what > >>> I want?" but instead to think "what do I want my programs to look like" > >>> and > >>> then design the language from there, reusing libraries as they seem > >>> helpful > >>> or designing new ones that do what you want. Racket's > >>> language-implementation facilities are pretty powerful (of course, if > >>> there > >>> is nothing like what you end up needing, there will still be actual > >>> programming to do ;). > >>> > >> > >> Thanks Robby -- that's a very interesting way to look at library design > >> that seems to make particular sense in the Racket environment. > >> > > > > An example of such an approach is racket-cas, a simple general purpose > > cas, which > > represents expressions as s-expression. > > > > The polynomial 4x^2 + 3 is represented as '(+ 3 (* 4 (expt x 2))) > > internally. > > > > The expressions are manipulated through pattern matching. Instead of > > using the standard `match`, I wanted my own version `math-match`. > > The idea is that `math-match` introduces the following conventions in > > patterns: > > > > This is also fascinating (and very useful) -- thanks. This package > illustrates the build-your-own-notation approach nicely. > [...] > > > Back to your project - what is the goal of the project? > > Making something like GAP perhaps? > > Do you want your users to supply types - or do you want to go a more > dynamic route? > > My project is really aimed at supporting self-directed learning of concepts > from abstract algebra. I was taught many years ago that to really > understand something to try implementing it in a high level language. That > will soon expose any hidden assumptions or misunderstandings. > > An early attempt (in Rust) is at: https://gitlab.com/ornamentist/un-algebra > > By using the Rust trait system (and later Haskell typeclasses) I could > create structure traits/typeclasses that don't clash with the builtin > numeric types or with the larger more production oriented libraries in > those languages in the same general area of math. > > Once I added generative testing of the structure axioms I could experiment > with, e.g. finite fields and ensure all the relevant axioms and laws were > (at least probabilistically) met. > > Thanks again Jens. You might also want to look at the implementations of category theory in Agda. Agda is a language which unifies execution and correctness proof to some extent. Not that you want to implement catagory theory, but category theory is a form of algebra, and you may find some useful ideas about syntax and semantics there. I attended an online seminar about this recently, but I haven't been able to find the details again. The following links seem to refer to the same project. (I found them looking for category theory in agda on duckduckgo. The software: https://github.com/agda/agda-categories Documents: Formalizing Category Theory in Agda pdf: https://arxiv.org/pdf/2005.07059.pdf slides: https://hustmphrrr.github.io/asset/slides/cpp21.pdf Agda itself is also worth a look. As well as older proof assistants like coq. There's definitely a trand towards constructivism in foundational mathamatics. -- hendrik > Stu > > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to racket-users+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/racket-users/b14e56eb-71ef-49f4-8e98-fea4ced6e3adn%40googlegroups.com. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/20210121135543.qi2rth7qkhlasrcc%40topoi.pooq.com.
Re: [racket-users] Unsafe structs
On 1/20/2021 1:53 AM, Sorawee Porncharoenwase wrote: However, ‘struct-field-info-list’ returns only fields defined by the actual type and does not include fields that were inherited. What I don’t see is any simple way to get at the struct’s inheritance hierarchy —- it seems that you have to iterate ‘struct-type-info’ to enumerate the supertypes. Yes, that’s a (the?) way to extract field names of supertypes. The reason I designed it in that way is that field name is a concept for each level in the hierarchy, not across levels. You can’t have two identical field names in a level, but you can have identical field names across levels. So lumping field names across levels together doesn’t look like a good idea to me. Yes, but fields defined in an ancestor are visible in its descendants. I understand the need to distinguish the individual types, but 'struct-type-info' does that already. IMO there should be an easy way to get information on *all* the fields at once - potentially including which supertype(s) defined them. YMMV, George -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/ba71e843-a3ae-d2ad-646d-27951b700485%40comcast.net.
