reuben364

One thing I realized that seq'ing too many things might be bad for performance. As I understand it,

   foldr1 (\x y -> ((x `par` delay 1) `seq` y)) $ map pure [1..]

Would require more and more comparisons over time. Is there some sort of codensity like trick that you can do? Or is this something the user of the library would worry about if it came to that. Or just have a redundant API.

Replying to your edit:

As I was writing it my headspace was that the duration was for seq to know when to switch. I wasn't really thinking about stopping the animation too.

(I also notices that my seq is wrong. The subsequent animation should start at the beginning, so it should be `g (t - df)`, not `g t`

I believe you are correct. Your implementation is more at the heart of what I wanted to show. . The main point I wanted to get across was the interface itself.

Thanks. I should have just clarified that I wanted to communicate the idea. I didn't expect to get it right first try.

Maybe I'll try and make a small library of it if there isn't already. I've never posted something on Hackage.

Basically auto playing anything for me is bad UX.

In Haskell, one can make more general combinators in the following way:

   type Anim a = (Duration -> a, Maybe Duration)

   -- Linear interpolation
   linear :: Anim Duration
   linear = (id, Nothing)

   -- Sequencing
   seq :: Anim a -> Anim b -> Anim (Either a b)
   seq (f, Nothing) g = (\t -> Left $ f t, Nothing)
   seq (f, Just df) (g, dg) = 
        (\t -> if t < df 
           then Left $ f t 
           else Right $ g t
        , df + dg)

   -- Parallelism
   par :: Anim a -> Anim b -> Anim (a, b)
   par (f, df) (g, dg) = (\t -> (f t, g t), max df dg)

   -- Constant
   pure :: a -> Anim a
   pure a = (const a, Nothing)

   -- EDIT: forgot delay
   delay :: Duration -> Anim ()
   delay d = (const (), d)

I know there's an Applicative in there, but I'm not sure where else this lies in the typeclass hierarchy.

EDIT: More fixes

EDIT: I should really test in GHCI before I post these things. But I'm lazy.

I'm no expert, but is there not cause for it being a language feature rather than a library? When you use a library you effectively have a DSL to construct your differentiable program, and lose the facilities of the host language.

It's also not quite declarative programming either. In the same way that you build ordinary executable programs out of smaller executable parts. You build differentiable programs of smaller differentiable parts. You aren't declaring what outcome you want, you are simply restricting what you are building your program out of so that it has properties that allow you to interpret the program differently from how it will run "normally".

I'm learning lean with that intent (to self learn mathematics). I get distracted trying to learn how to do better proof automation and tactic golf.

Also, since I don't see anyone mentioning so it far: there is a currently fairly active Zulip chat for the lean prover. They have been quite helpful for me getting started.

Adga does mixfix pretty well. A variable in scope can indicate the places for arguments with underscores (e.g. _+_ or _=<_>_). The tradeoff for being able to use pretty much any symbol in identifiers along with mixfix is that you have use whitespace (3 + 5, not 3+5). Though I agree it doesn't scale.

I far I am concerned, the most crucial aspect is my mind. I think, but wouldn't know how to prove, that the information needed to satisfactorily copy a human mind is finite. You may not be able to replicate quantum states, but can definitely replicate bits.

Unordered would be if cons(a, b) == cons(b, a) which is not the case

Well, a binary tree with unordered children.

I found the OPLSS lectures on parallel cost semantics using lambda calculus quite enjoyable, but I don't really know much about it.

https://www.youtube.com/watch?v=lSc0EtF6_Zk

I agree with the premise, not the argument

We can arrive at truth through dialogue, but dialog can also lead to propagation and affirmation of misinformation. One does not necessarily converge on truth.

Though, to entrust any government to control free speech to that end is an entire different point.

The point isn't that the deformed "cup" is the same as the original cup. It's that in the process of deformation the number of holes remains the same.

That's kind of a truism though. There will always be a non-zero entropy for the distinct kind of systems you want to build.

Unless there is one system to rule them all, configured exactly the way it is needed out the box.

That's a strawman. No one has stated that the success of AirBnB is easy to replicate, nor that a system of equal functionality is easy to create.

Lambas? That sounds amazing. :-)

Feels like a garden path sentence [1] targeted at developers

[1] https://en.wikipedia.org/wiki/Garden_path_sentence

Coq isn't very good for developing with properties encoded in the types. Such properties are defined seperately from the data structures involved.

The dependently-typed-ish features of haskell can provide a sweet spot of both untagged data along with the flexibility of heterogeneous lists.

That is the dependent typed aspect mentioned. This is actually done in Idris with VerifiedSemigroup and other verified instances.

Working my way through Software Foundations. Though that might not be considered programming.

My point stands. A non-endangered species is equally likely to yield useful insight as an endangered one.

Though I realise that I have made a weak argument and that I do have a, perhaps unreasonable, bias towards not expending effort to preserve endangered species. In my mind preservation of endangered species is hoarding on a larger scale: someday this species may be useful to us, so let us keep it around.

There are different types of value you can derive from these stories. There is the practical: crops that defend themselves from predators. Then there is entertainment value.

Arguing that practical value to be found in species past and present is akin to stating that all information can be found by in the digits of pi. Sure enough there are valuable things to find, but only amongst uninteresting things. Unless there is a mechanism to roughly draw out the interesting, such as evolution.

On the other hand, entertainment doesn't have a need to be fixated on anything particular. Details on the Dodo are lost, so you turn to the wasps. If the wasps are gone you turn to the snakes.

As for other types of value, I may miss something. Or our beliefs may fundamentally differ such that we cannot argue in terms of each others.

If you are saying print is gone, it isn't. It became a function in python 3.

   print "hello world"

became

   print("hello world")

If you are complaining about the format, then that really is a dumb reason.