Martin EscardoPeople who think their Agda code with no explanations is self-explanatory.
| www | https://tyde.systems/ |
| Pronoun’s | he/his |
| Locations | 🇳🇱 🏴 🇬🇧 🇪🇺 |
Jan de Muijnck-Hughes
@jfdm@discuss.systems
- 323 Followers
- 230 Following
- 2.5K Posts
Lecturer of type-driven approaches to trustworthy-systems (CyberSecurity) at Strathclyde. Professionally interested in PL & FM Methods; socially interested in coffee, politics, music, the outdoors, sci-fi, high fantasy, & much much more! My work doesn’t define me; it is not my identity.
I'm glad I am provoking you in the *right* ways...
That filter does look interesting, however, I'll need my Parliamo PigWorker/Agda book (and a clear head) to help truly get what you are cooking.
So yes, we should see what we can cook up.
PS:
I know not quite the same but:
https://github.com/jfdm/positively-negative/blob/main/Examples/Filter.idr
Oh... the image still from the video stops at an important slide!
Showing the Motivating Example Revisited...
Whilst I do not like tooting my own horn, if you were interested in my #TYPES2025 talk (Towards Being Positively Negative about Dependent Types) and could not make it.
Here you go:
TYPES2025 - 4.7. Jan de Muijnck-Hughes - Towards Being Positively Negative about Dependent Types
@consequently @mspstrath They didn't show the empty lectern for me.
It is hard to stay still when there is so much room to move...
I hear ICFP is going to get FREX'd but with the meeting of two conferences, fools seldom differ!
Well done all.
Reading up on #Python #typeAnnotations and #TIL that Python 3.12+ makes it a lot easier to define generics:
```
def safeHead[T](xs : list[T]) -> None | T:
pass
```
https://mypy.readthedocs.io/en/stable/generics.html#generic-functions
I didn't realise that as my system runs python3.10 (LTS ¬FTW; Support only upgrades at end of service life).
Need to explore how to get python3.12 running locally and not breaking my system.
Oblomov
@tonyg ‘match value’