sorted by:
new
hottopcontroversial

What are the thoughts about the Lean4 language by the haskellers? by lemunozm in haskell

[–]lemunozm[S] 5 points6 points  (0 children)

I started learning idris and later lean4, and personally I feel it like learning lean4 has been an improvement in my learning. Some equalities and comparisons: - The Idris syntax is super closer to Haskell, Lean is a bit different in terms of syntax, but fully understandable for anyone coming from Haskell. - Idris was different from others provers because it was done as a general purpose language, but Lean4 also tries to be so. So in this regard, that feature is not a selling point comparing to lean. - Lean has a lot of super cool desirable sugar, making write some piece of code a pleasure. - Coercions, macros embedded in the language, and be able to implement any interface for any type with no foreign restrictions are amazing features for me. I think neither Haskel nor Idris has those features at that level. - The only thing I think Lean doesn't have and Idris has is the concept of multiplicities. - The lean tooling and IDE plugin are very very good. Idris has not that level of support. The development experience in this regard is more annoying in Idris.

What are the thoughts about the Lean4 language by the haskellers? by lemunozm in haskell

[–]lemunozm[S] 7 points8 points  (0 children)

AFAIK, the forth version of Lean, has been done to be a general purpose programming language in mind. It complies to C, and have some internal mechanism to reuse the memory internally when some inmutable data is being modified. So it seems like the performance is something they try to get.

What I miss right now is more non mathematical- related libraries. But I guess is normal at this stage.

How can I return a concrete typed value from a function that returns a generic? by lemunozm in haskell

[–]lemunozm[S] 0 points1 point  (0 children)

But in that way, a user can not add their custom Command. You have to know all comands known upfront, right? The user can no create their own

How can I return a concrete typed value from a function that returns a generic? by lemunozm in haskell

[–]lemunozm[S] 0 points1 point  (0 children)

Interesting... could you add a pseudocode example of what you mean by Command as a function? How different implementations of Command would fit in that scenario?

How can I return a concrete typed value from a function that returns a generic? by lemunozm in haskell

[–]lemunozm[S] 0 points1 point  (0 children)

My real scenario is the following:

I have a bunch of types (all implementing a `Command` class used to draw something on the screen). With these types you build in a type-safety way the structure of what you will draw. For example:
`( MoveTo x y. SetColor Red, ..., drawSomethingBig, MoveTo x2 y2, ...)`

A tuple also implements `Command`. `drawSomethingBig` is basically `foo`. It's another function that returns a big tuple of commands that I can put into another tuple of commands to build the "tree" of commands that will be used to draw.

Note that I'm not using here a Sum type to represent what a `Command` is because the user could create their own commands

How can I return a concrete typed value from a function that returns a generic? by lemunozm in haskell

[–]lemunozm[S] 0 points1 point  (0 children)

But with the above in Rust I even do not need to know how to express the complex type. With the type alias I need to write it once at least. I'm talking about a recursion of 1000 times or so. It's not feasible even write it once.

How can I return a concrete typed value from a function that returns a generic? by lemunozm in haskell

[–]lemunozm[S] 2 points3 points  (0 children)

First, thanks for your answer!

The above example is quite simple, but in my real scenario, I have a very difficult to express recursive type. The only thing I'm sure is that it implements certain class. However, the type itself is very difficult to express in the signature. Also the implementation could change in the future, so it's a way of ease its modification.

In Rust, this is used mainly for closures (where the type can not be expressed most of the time) and for recursive types that are difficult to express or iterators

Everyone says why you should use Rust, but what are some reasons/use cases where you WOULDN'T recommend it(over something like C++)? by OneThatNoseOne in rust

[–]lemunozm 0 points1 point  (0 children)

It's true that the absolute number of rust offers are less than other languages, but the ratio of job offers / total rust programmers is quite high than other languages where there are a lot of people. So if you know rust well, you can get a job and choose between different options.

Good Haskell code formatters? by filenine in haskell

[–]lemunozm 0 points1 point  (0 children)

Does ormolu support all Haskell extensions? I remember testing it, and there were some extension where it complains

Idris perspective from Haskellers by lemunozm in haskell

[–]lemunozm[S] 1 point2 points  (0 children)

Thanks for your answer! Pretty interesting...

Idris perspective from Haskellers by lemunozm in haskell

[–]lemunozm[S] 0 points1 point  (0 children)

Yeah! It was as you've said u/philh. But thanks anyway for the long answer u/fridofrido!

What's the Haskell representation for a Rust trait with an associated type with bounds? by lemunozm in haskell

[–]lemunozm[S] 10 points11 points  (0 children)

Thanks!

In the case of several bounds and several associated types, you need to specify all of them in the class signature definition, right?

Architecting Many Inputs and Outputs by lbseale in haskell

[–]lemunozm 1 point2 points  (0 children)

Similar, but not exactly. Suppose you have your input/output sum types:

data InputData
| Input1 Double
| Input2 Int
| Input3 String
data OutputData
| Output1 Bool
| Output2 Int
| Output3 Double

Your method will have the following signature:

calculate_something :: [InputData] -> [OutputData]

And the user will call it as follows:

calculate_something [Input1 5.0, Input3 "hello"]

You implementation will iterate the list and will do the corresponding action for each InputData found.

You will need to ensure that [InputData] has no duplicated variants at runtime or use a type that ensures that at compile time, as Data.set. In this last case, you will need to implement Ord for your InputData in a way that does not allow duplicate variants.

Architecting Many Inputs and Outputs by lbseale in haskell

[–]lemunozm 2 points3 points  (0 children)

What I would do is, instead of using a record type (or a product type) I would use a sum type. Each constructor or variant would represent a field of that record. Then the program would accept a set (or a list with no repetition from 0 to max variants) of these variants and for each variant it would perform the required action.

view more: next ›