IRCBrowseLink
2025-06-02 18:50:04 +0200 <miguelnegrao> it would be pretier
2025-06-02 18:50:41 +0200 <tomsmeding> well, perhaps it would, but I'm fairly sure it's impossible to give `use` a type that makes that work
2025-06-02 18:51:02 +0200 <miguelnegrao> ok, that is good to know. I just felt a bit stupid writting it over and over :-)
2025-06-02 18:51:14 +0200 <miguelnegrao> glad to know the problem is not on my side
2025-06-02 18:51:27 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-02 18:51:50 +0200 <tomsmeding> there are other languages that do allow partial application of "type families"; in particular, Agda and Idris
2025-06-02 18:51:50 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-02 18:52:24 +0200 <tomsmeding> but that's a whole different territory :)
2025-06-02 18:52:42 +0200 <miguelnegrao> Another thing I have a feeling I cannot do is compile a list of proofs and tell GHC to use all those proofs to prove something else.
2025-06-02 18:53:06 +0200 <tomsmeding> data Dict c where Dict :: c => Dict c
2025-06-02 18:53:06 +0200 <miguelnegrao> I have to write it like: gcastWith p1 $ gcastWith p2 $ gcastWith p3 $ Refl
2025-06-02 18:53:12 +0200omegatron(~some@user/omegatron) (Quit: Power is a curious thing. It can be contained, hidden, locked away, and yet it always breaks free.)
2025-06-02 18:53:23 +0200 <tomsmeding> then use `Dict @(a :~: b, c :~: d, e :~: f)`
2025-06-02 18:53:27 +0200 <miguelnegrao> I did rename gcastWith to "have" so it looks a bit better
2025-06-02 18:53:40 +0200 <tomsmeding> to bundle up a bunch of proofs
2025-06-02 18:53:48 +0200 <tomsmeding> but it's not generic like passing a list of proofs, no
2025-06-02 18:53:49 +0200 <miguelnegrao> interesting
2025-06-02 18:54:41 +0200 <tomsmeding> but that may help only if you have the same set of "lemmas" in a bunch of places
2025-06-02 18:54:44 +0200 <miguelnegrao> Thanks tomsmeding for that tip, I will investigate
2025-06-02 18:55:20 +0200 <miguelnegrao> No, usually I just build a group of substeps in the proof which I then use in a more complicated expression part of the same proof
2025-06-02 18:55:42 +0200 <tomsmeding> is the goal of this just to play around with singletons in haskell?
2025-06-02 18:55:53 +0200internatetional(~nate@2001:448a:20a3:c2e5:5e5:e8fb:73b6:1daa) internatetional
2025-06-02 18:55:59 +0200 <tomsmeding> because if the goal is to formalise some mathematics, haskell is _not_ the suitable language :p
2025-06-02 18:56:15 +0200 <miguelnegrao> Essentially yes, it is just for fun
2025-06-02 18:56:23 +0200 <tomsmeding> then have at it :)
2025-06-02 18:56:29 +0200 <miguelnegrao> But I have been porting mathlib, the Nats part
2025-06-02 18:56:52 +0200 <miguelnegrao> stuff like theoremAddMulDivLeft :: forall x y z . SNat x -> SNat y -> SNat z -> N0 < y -> (x + (y * z)) / y :~: (x / y) + z
2025-06-02 18:57:01 +0200 <dolio> Translating mathlib to Haskell is going to be very painful, I expect.
2025-06-02 18:57:07 +0200 <miguelnegrao> YES !
2025-06-02 18:57:22 +0200 <miguelnegrao> comutativity and associativity is very painful
2025-06-02 18:57:47 +0200 <miguelnegrao> but it puts me in a zen state I guess
2025-06-02 18:57:54 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-02 18:58:17 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-02 18:59:31 +0200 <EvanR> associativity was a mistake, lisp was right, just use gratuitous amount of parentheses
2025-06-02 18:59:53 +0200 <miguelnegrao> In proofs you have to move every single parenthesis manually...
2025-06-02 19:00:14 +0200 <miguelnegrao> (a + b) + c is not equial to a + (b + c) unless you use a proof of that...
2025-06-02 19:00:49 +0200 <Leary> miguelnegrao: Suggestion: declare `pattern QED = Refl; (==>) = gcastWith; infixr 1 ==>` and write `p1 ==> p2 ==> p3 ==> QED`.
2025-06-02 19:01:07 +0200internatetional(~nate@2001:448a:20a3:c2e5:5e5:e8fb:73b6:1daa) (Remote host closed the connection)
2025-06-02 19:01:19 +0200 <miguelnegrao> oh, I like that !
2025-06-02 19:01:25 +0200internatetional(~nate@2001:448a:20a3:c2e5:5e5:e8fb:73b6:1daa) internatetional
2025-06-02 19:02:18 +0200internatetional(~nate@2001:448a:20a3:c2e5:5e5:e8fb:73b6:1daa) (Client Quit)
2025-06-02 19:03:29 +0200miguelnegrao(~miguelneg@2001:818:dc71:d100:97a9:f15a:6ac:fc9e) (Quit: Client closed)
2025-06-02 19:03:40 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-02 19:04:06 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-02 19:04:43 +0200tromp(~textual@2001:1c00:3487:1b00:7d34:d696:3458:218b) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-06-02 19:06:19 +0200 <ski> hellwolf : i didn't bring up existentials. however, in logic, you often define `Not a = a -> Void' (`Void' being the false proposition (the nullary disjunction), having no proof, but having an elimination rule, with zero branches, in Haskell terms effectively `void :: Void -> a; void v = case v of {}'). however, if you don't use the elimination, you can replace `Void' with an arbitrary proposition `o'
2025-06-02 19:06:25 +0200 <ski> (giving you "minimal logic", rather than "intuitionistic logic"), so instead of `Not (...)' you'd have `... -> o'
2025-06-02 19:08:07 +0200orcus-(~orcus@user/brprice) (Quit: ZNC 1.8.2 - https://znc.in)
2025-06-02 19:08:08 +0200dispater-(~dispater@user/brprice) (Quit: ZNC 1.8.2 - https://znc.in)
2025-06-02 19:08:31 +0200 <__monty__> And that's because o *could* be Void?
2025-06-02 19:09:51 +0200dispater-(~dispater@user/brprice) brprice
2025-06-02 19:10:22 +0200orcus-(~orcus@user/brprice) brprice
2025-06-02 19:10:55 +0200 <EvanR> because parametricity stops you from ever producing an o, Void or not
2025-06-02 19:11:20 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)