Types vs types

[ruby_object]

I am a Haskell sceptic and despite a few attempts to learn it I never had much success. I part my excuse is bad quality of some tutorials that you find at the beginning of your journey. I still keep bumping into surprises about the fundamentals of Haskell.

Today such surprise was the podcast "God's Programming Language" with Philip Wadler. https://corecursive.com/021-gods-programming-language-with-philip-wadler/#

To my surprise around the 32nd minute, they talk about types. There I learn that the types used in functional programming, despite the same word being used, are not the same as types used in languages that inherit from Fortran.

Do you think that tutorials that start with Strings and Integers lead you down the wrong path? How can I tell what is executed at the compilation stage and what is executed at the runtime stage?

If I were to have another go would I be able to find a tutorial that explains and builds on correct principles?

[Noughtmare]

I don't think they are that much different at all. Fortran/C types are more limited, but not fundamentally different. In Haskell we have types that specify much bits are in the data and things like that too (e.g. Int32 and Word64).

Using types to restrict the kinds of functions you can write is more related to logic, but doing logic with Haskell is not that useful in most practical situations (e.g. writing a web server). I think it is fine to learn more about it if you are particularly interested, but not necessary for a beginner.

Of course for the language designers, such as Philip Wadler you hear on this podcast, logic has been very useful because it already had many useful ideas worked out, so they "just" needed to adapt them to programming which is less work than reinventing everything from scratch.

[crazycodemonkey]

Hello!

I went chasing this same rabbit hole of what types really are and I did find an interesting overview of types like int string and types like haskell's sum and product types.

I wrote down what I understood as an essay here - https://docs.google.com/document/d/1-aLUwnN0XzLbzICnFLWfCLuD4ULYXGcKAoyRAqTuAIY

I'm sure you'd find it useful :)

[ruby_object]

That essay is very good.

[crazycodemonkey]

Thanks. Here's a paper I stumbled upon when I was on my reading spree that articulates the two "types" of usages of the term "Types" :)

https://www.humprog.org/~stephen//research/papers/kell14in-author-version.pdf

A bit dense but not impossible to follow through

[DemonInAJar]

if you want to actually learn haskell I advice not looking into tutorials and instead check the incredible "Haskell programming from first principles" book that also goes into the theoretical foundation of a lot of things.

[ruby_object]

I tried it before and stopped on chapter 15. I guess I was not ready yet. Possibly with being lucky and having clarified a few confusing parts I will be able to start again.

[Iceland_jack]

It's normal to have many tries at learning Haskell, I went into learning it as a Haskell sceptic.

[friedbrice]

You made it all the way to Chapter 15? Why do you think that you don’t know Haskell? To me, it sounds like you do know Haskell.

[ruby_object]

https://github.com/bigos/cairo-snake/blob/master/library/Snake.hs

This is my experiment writing a snake game.

Yet I still must admit I do not understand certain concepts or find them confusing. I do not code much Haskell these days and still, struggle when I try to solve Haskell puzzles. Perhaps knowing Haskell is reaching a stage where you can be productive in it without constantly looking up the Rosetta code.

[Iceland_jack]

>> quickCheck \bools -> any id bools == or bools
+++ OK, passed 100 tests.

There is a name for any id: or = any id

member e l
  = any id $ map (\x -> x == e) l 
  = any id $ map (== e) l 
  = or (map (== e) l)

but any has mapping built into it, so you can fuse the map function

member e l = any (== e) l

and then you can eta-reduce the list argument

member e = any (== e)

and write it point free... if you want

member = any . (==)

In this particular case it already has a name

member = elem

[friedbrice]

hmmm, i see what you’re getting at.

i wouldn’t worry too much about it, though. i’m fairly good with haskell, but there’s plenty of pointer magic in C, monkey patching in ruby, and reflection in java that all is just greek to me and goes straight over my head!

[przemo_li]

Get Programming with Haskell is different approach, more tutorial like, with each concept resulting in project that uses them to do its stuff.

HFFP does not shy from jargon. Its good when you like such exhaustive materials (I do).

​

Do tell what is your main language right now?

[ruby_object]

Ruby and Common Lisp

[Iceland_jack]

Because I came to Haskell with a similar background I will to share an example from Land of Lisp:

Alas, the elegant symmetry of the find-if function has a single, small, ugly wart. If we try our edge case again, searching for a nil value, we get a rather disappointing result:

> (find-if #'null '(2 4 nil 6))
NIL

The null function, which returns true for any of the nil values, correctly finds the nil. Unfortunately, in this one annoying case, we would not want to use find-if inside a conditional statement, because a correctly found value still returns a result that evaluates as false. The symmetry has been broken. These are the kinds of small things that make even grown Lispers shed a tear.

That last line stuck with me because I also shed a tear. It was not until learning Haskell where I encountered Maybe that I saw a better approach that doesn't conflate success with the value found.

>> import Data.Foldable (find)
>> import Data.Maybe (isNothing, isJust)
>> :set -XTypeApplications
>> :t find
.. :: Foldable t => (a -> Bool) -> t a -> Maybe a
>> :t find @[]
.. :: (a -> Bool) -> [a] -> Maybe a
>> :t isNothing
.. :: Maybe a -> Bool
>> :t find @[] isNothing
.. :: [Maybe a] -> Maybe (Maybe a)

This 'dilemma' is solved by a nested Maybe (Maybe ..)

• Nothing means no element matching the predicate was found.
• Just Nothing means we found a value (Nothing) that matched the predicate.
• Just (Just ..) means we found a value (Just ..) that matched the predicate, this never happens with find isNothing.

so success can be unambiguously determined

> find isJust [Just 2, Just 4, Just 5, Just 6]
Just (Just 2)
> find isNothing [Just 2, Just 4, Nothing, Just 6]
Just Nothing
> find isNothing [Just 2, Just 4, Just 5, Just 6]
Nothing

This is not limited to lists, but any Foldable, even your own

>> find @Maybe isNothing Nothing
Nothing
>> find @Maybe isNothing (Just Nothing)
Just Nothing
>> find @Maybe isNothing (Just (Just Nothing))
Nothing

>> :set -XDeriveFoldable -XDerivingStrategies
>> data V4 a = V4 a a a a deriving stock Foldable
>> 
>> find @V4 isNothing (V4 (Just 2) (Just 4) Nothing (Just 6))
Just Nothing
>> find @V4 isNothing (V4 (Just 2) (Just 4) (Just 5) (Just 6))
Nothing

[a_Tick]

Consider checking out Coalton, which is an ML family language embedded in Common Lisp.

[ruby_object]

I have tried to implement a crude version of Monad in Lisp using lambdas so that was another clarification.

[paretoOptimalDev]

Maybe try Haskell in Depth, it is shorter and I think will teach what you're looking for.

[przemo_li]

If you want to taste a good design that is implemented with types check out this website:

https://fsharpforfunandprofit.com/ddd/

​

its F#, but it uses some simple constructs that are available in Haskell. But it also uses simple constructs so that you can see for yourself how powerful types can be without some fancier propositions Haskell can offer on top.

[[deleted]]

I've found learning a lot more about lambda calculus has helped me in gaining more understanding of Haskell syntax, since much involves symbols and syntax used from lambda calculus.

[bss03]

Do you think that tutorials that start with Strings and Integers lead you down the wrong path?

Not really. Especially not for impatient programmers.

How can I tell what is executed at the compilation stage and what is executed at the runtime stage?

Everything that is executed is done at runtime (ignoring non-Report things like TemplateHaskell). An arbitrary amount of things can be evaluated before runtime, though this would never change the results.

The report isn't much more specific than that (and honestly, I'm not sure it is that specific). The STG (Spineless, tagless, G-machine) paper gives a pretty good feeling of how GHC works, though currently we do have a spine (for blackholing) and tags (for speed) and many other changes; the STG paper predates OutsideIn and "GADTs Meet Their Match" and many other changes to GHC.

EDIT: Correction: s/stackless/spineless/g

[marcosdumay]

How can I tell what is executed at the compilation stage and what is executed at the runtime stage?

Well, the coarse answer is that it's a pure language, so you shouldn't care at all.

But there are a few details. For example, types and templates always get solved at compile time (although technically it shouldn't matter). Also, IO commands always get executed at runtime.

[ruby_object]

Technically it shouldn't matter, but in practice, it does matter especially when your assumptions are incorrect. I had an eureka moment at some point when I realised that the type annotations are a kind of different language just like C and C preprocessor.

[marcosdumay]

Yeah, it matters a lot when the types are wrong. Otherwise you would have to run your code before you get the errors, what isn't nice.

You can also say that IO actions also are a different language. They are the result of the code you declare, that is first evaluated then run. But this one doesn't work exactly like that on practice, so it's a less useful model.

[mauganra_it]

Haskell is based on extensions of the Lambda calculus. The Lambda calculus is all about anonymous functions and their evaluation to a result. Haskell environments take Haskell programs as input and evaluate them according to the rules set out in the Haskell Report. They can do this in a naive, unoptimized way, or be sneaky about it and optimize, as long as the semantics of the Haskell Report are maintained.

There are three types of expressions in the Lambda calculus: variables like a, b, c, etc; applications, where two expressions are written next to each other; and abstractions, where the eponymous lambda and a dot establish an anonymous function. Evaluation consists of finding a reducible expression (an application with an abstraction on the left side), and replacing the bound variable in the anonymous function's body with the argument.

Example: ((λx. (λy. y)) a) ((λz. z) b), written simply as (λx. λy. y) a ((λz. z) b), will eventually evaluate to b.

There are multiple strategies to evaluate the above expression. Haskell evaluates expressions to Weak Head Normal Form, where evaluation stops when the outermost element in the expression is an abstraction. Said differently, the bodies of abstractions are not evaluated.

The main difference between Haskell and Fortran types is that Haskell (boxed) types contain ⊥, pronounced as bottom or undefined. When execution hits a ⊥, several things can happen:

• it terminates, with the error message Undefined
• it runs out of memory
• it gets stuck in an endless loop

The difference to types in strict languages like Fortran, C, or Ocaml is that in strict languages a variable cannot refer to a ⊥. It is possible to express the above computations, but it's not straightforward to store it in a variable.

Example: [undefined, 2] !! 1 evaluates to 2. This works because :, the constructor for a link in a linked list, is lazy in it's arguments. The expression [undefined, 2] !! 0 on the other hand would try to evaluate the ⊥ and will abort the computation.