Jons Mostovojs @jonn@social.doma.dev

@SnowshadowII I just hope we won't find strange bedfellows in what's coming. I already feel like Turkey with it's democracy-washed autocracy will have to be our best friend, haha.

Oh how wrong I was about European defense industry in 2010s. With threats from both russia and usa, it seems like we are already too late to defend ourselves.

But we shall put on a fight.

@knotfeed a very sick heart indeed

@tolmasky the amount of times I had to learn what is #CommonJS and what is #ESM to then forget it and get bitten again when I come to #JS is bleak in comparison, I'm sure, but it made me make a video (mostly for myself) to later watch: https://www.youtube.com/watch?v=SIows5N4BAY

😆

@tolmasky if I had to implement reflection in Lean4 or Agda, I would try to mimic #Haskell's typeable.

But also, I think there must be a very important point here! In dependently typed languages, entities can have more than one type!

(frac 1 2) : Frac 2 4, but also (frac 1 2) : Frac 4 8, for instance.

[1] : ListLE 1, but also [1]: ListLE 42.

So, perhaps the whole idea of general reflaction is defeated by this property. And this is why #haskell offers superior reflection[1]. Note that #Typeable is in #GHC itself!

I don't know if I'm mansplaining here or if you're aware of haskell's Typeable, but here is a simple demo of its capabilities: https://github.com/cognivore/typeable-haskell-demo/blob/main/app/Main.hs

In #Lean, I would emulate it by defining asking the user to provide explict instances over an enum, just as you wrote! The existential quantification trick can be done in #Lean by carrying the instance inside a structure that ties the knot between the type and an entity which has this type:

```
structure Stuff where
α : Type
val : α
inst : Reflect α
```

You won't be able to construct it unless α is Reflect.

* * *

[1]: https://hackage.haskell.org/package/base-4.21.0.0/docs/Type-Reflection.html#t:TypeRep

@tolmasky fwiw, you are absolutely correct: https://lean-lang.org/lean4/doc/dev/ffi.html?highlight=import#the-lean-abi

@tolmasky ah! "Type-safe version of reflection" makes a lot of sense. I will think more.

@tolmasky I didn't go into details of your use-case, sorry, but the mind-bending bit about dependently typed languages is that there are no value-type dichotomy. Just sone expressions with those are expressible, and some are not.

I take a lot of pride in this code:

https://github.com/argumentcomputer/Wasm.lean/blob/main/Wasm/Wast/Num.lean#L85-L89

Observe how function invocation is a type. (Feel free to ignore Cached constructor, it's an optimisation).

Sorry for a non-answer, I hope it helps. But based on what I understand about the things you describe, it should be somehow possible and I hope my snippet will get you moving in the right direction.

I hope that the West (whatever that word means anymore) is happy. Trump going ape-shit is the direct consequence of insufficient actions taken to stop putin. Dictators and wannabe dictators are watching and learning.

@mudkip I say. Fancy a cuppa?

https://www.youtube.com/watch?v=50_Ddhfbj_Q

#FunnyWays #Progressive #Prog #ProgRock #GentleGiant

This song makes me cry sometimes. ❤️