Geek Answers Handbook

Fat arrow in Idris

I hope this question is suitable for this site, it’s just a choice of specific syntax in Idris compared to Haskell, as both are very similar. I think this is not so important, but I'm very interested. Idris uses =>for some occasions when Haskell uses ->. So far I have seen what Idris uses ->in function types and =>for other things like lambdas and case _ of. Has this choice gained the recognition that in practice it is useful to have a clear syntactic difference between these use cases? Is this just an arbitrary cosmetic choice, and I overdid it?

+6
source share
2 answers

Well, in Haskell, the types of signatures and values ​​are in different namespaces, so something specific in one does not run the risk of colliding with something else. In Idris, types and values ​​occupy the same namespace, so you do not see, for example. data Foo = Foo, as in Haskell, but data Foo = MkFoo- the type is called Foo, and the constructor is called MkFoo, because there is already a value (type Foo) associated with the name Foo, for example data Pair = MkPair http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html #tuples Therefore, perhaps in the best way, he did not try to use the arrow used to construct the type of functions, with the arrow used for lambda - these are completely different things. You can combine them, for example. the (Int -> Int) (\x => x).

+4
source

, , -> -. Wikipedia:

A => B , A , B ; A false, B

case,

-> , =>, ,

f: X -> Y , f X Y

, -> , .. , Haskell , , =>.

0

More articles:


All Articles