/fpt/ - Functional Programming Thread

File: Calculus of Maki Constructions.png (312KB, 452x355px) Image search: [Google]

312KB, 452x355px

>Lisp girl
Please use a functional programming related anime image next time

>>58244751
Haskell was created because a lot of people had a lot of similar FP ideas that they kept incorporating into their own languages, but it's a lot better if it's consolidated into a single language.
Haskell's extensions make it a great place for language designers to experiment with new language constructs, typing mechanisms, syntax, etc.

Besides, it's by far the most popular purely functional language. Languages like OCaml just don't have that much going for it.

>>58244837
Homotopy type theory is always presented as Martin-Loef type theory, not as a pure type system.

>>58244947
Hott is an extension of MLTT. whats your point even?

File: 1482055600767.png (818KB, 1280x719px) Image search: [Google]

818KB, 1280x719px

>>58244837
>Maki
>ever
Karen best girl.
Exactly this picture made me create the first /fpt/ ever.

t. Creator, splitter and autist OP

>>58244982
Maki is holding the HoTT book but has a CoC overlay.

>>58244574
There are no closures in SKI calculus, and K is fundamental.

i.e., you don't need closures for 'const'. Closures are just environment capture. If you don't have a environment, you can't capture it.

>>58245149
So would it be more accurate to say that FP really needs some mechanism of partial application? That applies to both lambdas and combinators.

>>58245169
I thought you might be confusing closures with some other concept.

After using Eclipse for over a year I just recently switched to IntelliJ. Why didn't anybody tell me how it was THAT much better. Everything is so smooth I almost want to lick my screen.

>>58245201
I'm a different poster, I'm relating this back to >>58243857.

>>58244993
Yeah, well you know what?
I made that image, so I made you who you are

>>58245218
Yup. You don't need closures for functional programming. Closures only come about as a result of first-class functions in combination with lexical scope.

While it's pretty hard (understatement) to claim a language is 'functional' without first-class functions, it's definitely possible to have dynamic (as opposed to static) scope.

That said, Joy is arguably a 'functional language' without first-class functions (which are instead emulated using quoting).

>HaskLEL is useless and, pure functional and stateless languages are a meme
>Lisp is only used for third class text editors
>SICP is not a good book and this is why it's given away for free
>Anime is shit
>Maki a slut
>C++ is much better than C
>Java is the language of the future
>JS is a good choice for server side
>The best software engineers are indians

>>58245314

post = "R" <> e
  where
    e = "E" <> e

File: FnFgoLs.jpg (134KB, 778x1018px) Image search: [Google]

134KB, 778x1018px

>>58244769
>no Higher Order Perl

>>58245169
>So would it be more accurate to say that FP really needs some mechanism of partial application? That applies to both lambdas and combinators.
Hmm.. yes i think that's fair to say. to "have higher order functions" in a category sense is to have an isomorphism from HOM (a*b, c) to HOM(a, c^b); a way to go back and forth between curried and uncurried functions. there are platform dependent ways to do that, but, to say a function pointer is an exponential, you'd need some way of converting between (C*)(A,B) and (((C*)(B))*(A)), which you can't do with just standard C. You could use a different type for your exponential, and call 'higher order functions' not pointers to functions, but whatever 'partially applied functor' thing you've defined to do that instead.

>>58245314
>>HaskLEL is useless and, pure functional and stateless languages are a meme
>>Lisp is only used for third class text editors
>>SICP is not a good book and this is why it's given away for free
>>Anime is shit
>>Maki a slut
>>C++ is much better than C
These are actually true.

>CS 1 teacher worked at glaslow for several years
>world class haskell user
>offering a class on haskell
>its extraciricular meaning it wont count for credits

Should I go for it?

>>58245494
Who is it?

>>58245494
Yes
>its extraciricular meaning it wont count for credits
Who the hell cares.

>>58245494
Yes.
It's useful.
You can always tell employers you know it.

>>58245494
I want to go

File: sss.jpg (51KB, 453x504px) Image search: [Google]

51KB, 453x504px

Do you associate languages with colors? As in, when you see a bunch of code or even aren't looking at anything in particular but are just thinking in that language, does it have a certain tint for you?

For me it's

Lisp: Green
Haskell: Red
OCaml: Blue

File: st george's cross.png (5KB, 1280x768px) Image search: [Google]

5KB, 1280x768px

>>58245612
Haskell: Red and White

>>58245612
Haskell is violet,
F-Sharp is blue.
Happy New Year,
Anon, I love you!

>>58245347
> (<>) is string concatenation
> (<>) is not an inequality check
your language a gay
>>58245696
that's just the logos nerd

>>58244769
Functional poorgramming is a joke.

>>58245612
Lisp is yellow, Haskell is blue (and grey and purple to lesser extents), OCaml I try not to think about.

>>58245704
> (<>) is string concatenation
Oh dear, Anon, you have a long way to go.

>>58245704
She just told you she loves you and you call her a nerd?

>>58245704
(<>) is just any binary associative operation on algebraic objects with a monoidal structure.

>>58245704
/= is best inequality. Go back to shitcaml you scrublord

>>58244769
Thanks OP for adding the second Haskell book. I've been trying to find it.

>not using FiraCode so != looks like ≠

>>58245867
What the hell is a FiraCode and why aren't you using emacs where you can configure anything to look like arbitrary unicode symbols?

File: 1471988524111.jpg (121KB, 734x549px) Image search: [Google]

121KB, 734x549px

>>58245704
>>58245726
>>58245787

>>58245994
a font

baka

Nat : Size => Type
zero : Nat i
succ : Nat i => Nat $i

Nat i = (x : {
    zero : F .zero,
    succ : [i' < i] => (m' : Nat i') => F (.succ m')
} => F x)
zero h = h.zero
succ m' h = h.succ m'

add : Nat i => Nat j => Nat #
add m n = m {
    zero = m,
    succ n' = .succ (add m n')
}

Thoughts?

>>58246331
Language?

>>58246378
One that does not exist yet. Also I fucked up:

add : Nat i => Nat j => Nat #
add m n = n {
    zero = m,
    succ n' = .succ (add m n')
}

>>58246397
What are you going to use to implement it?

>>58246429
Probably Haskell.

>>58246453
Yeeeeeahhbuddy.

>>58246500
Is it understandable enough? It uses self typing (x : F x) and sized types for termination checking but otherwise it's pretty standard.

>>58245726
>>58245787
sounds like a gay language, just use (++) for that

>>58247085
Trolled hard.

>>58246524
it seems pretty weird at first glance. like what is $i and #? I do like the pattern matching syntax a lot though

>>58247172
That's taken from the MiniAgda sized types syntax. $ is successor and # is infinity.
https://arxiv.org/pdf/1012.4896

>>58245612
Haskell: Green
Lisp: Yellow
OCaml, F#: Orange
Erlang: Red
-
C: Black

whatever happened to lainchan?

>>58247263
It's alive, and very, very*, slow.

*very

>>58247313
The Haskell thread is dead

I hope that I'm not late. If your language doesn't implement dependent type it's not a true fp.

Definition U : nat -> Type -> Type :=
  fix f (n : nat) (T : Type) {struct n} : Type :=
  match n with
  | S n => T -> f n T
  | 0 => T
  end.

Definition sum : forall n : nat, U n nat :=
  let f :=
    fix f (n accu : nat) {struct n} : U n nat :=
    match n with
    | S n => fun x => f n (accu + x)
    | 0 => accu
    end in
  fun n => f n 0.

Eval compute in sum 3 100 10 1.

>>58247449
Name a dependently typed language with at least mediocre performance.

I'll wait.

>>58247466
You can compile the rooster to caml if you want. So performance is not a problem.

>>58247466
ATS

File: 1465745950049.png (602KB, 963x720px) Image search: [Google]

602KB, 963x720px

>>58247479
>You can compile to caml so performance is not a problem

>>58247202
interesting. IMO the syntax is a bit too terse in that case, but idk how to make it more descriptive without making it Java
>>58247490
literally faster than any other FP language
>>58247466
Ur, ATS, F* possibly

>>58247511
>idk how to make it more descriptive without making it Java
You could upgrade to full Presburger arithmetic (so addition instead of just successor) and it would still be automatic.

You could go even further and use Nat (which is how you do advanced termination proofs in Agda) but it just gets ugly at that point.

>>58247490
Let me show you my dear blonde anon:

Definition U : Type -> nat -> Type :=
  fix f (T : Type) (n : nat) {struct n} : Type :=
  match n with
  | S n => T -> f T n
  | 0 => T
  end.

Definition sum :
  forall (T : Type) (add : T -> T -> T) (zero : T) (n : nat), U T n :=
  fun T add zero =>
  let f :=
    fix f (accu : T) (n : nat) {struct n} : U T n:=
    match n with
    | S n => fun x => f (add accu x) n
    | 0 => accu
    end in
  fun n => f zero n.

Extraction Language Ocaml.
Extraction "sum.ml" sum.

After compiling that file the file sum.ml contains

type __ = Obj.t

type nat =
| O
| S of nat

type 'x u = __

(** val sum : ('a1 -> 'a1 -> 'a1) -> 'a1 -> nat -> 'a1 u **)

let sum add zero =
  let f =
    let rec f accu = function
    | O -> accu
    | S n0 -> (fun x -> Obj.magic f (Obj.magic add accu x) n0)
    in f
  in
  (fun n -> Obj.magic f zero n)

So you can have fast proved code.

>>58247603
Abetter version with int instead of the slow type nat.

Definition U : Type -> nat -> Type :=
  fix f (T : Type) (n : nat) {struct n} : Type :=
  match n with
  | S n => T -> f T n
  | 0 => T
  end.

Definition sum :
  forall (T : Type) (add : T -> T -> T) (zero : T) (n : nat), U T n :=
  fun T add zero =>
  let f :=
    fix f (accu : T) (n : nat) {struct n} : U T n:=
    match n with
    | S n => fun x => f (add accu x) n
    | 0 => accu
    end in
  fun n => f zero n.

Extraction Language Ocaml.
Extract Inductive nat => "int"
  [ "0" "(fun x -> x + 1)" ]
  "(fun zero succ n -> if n = 0 then zero () else succ (pred n))".
Extraction "sum.ml" sum.

>>58247603
>>58247707
ew

>>58247777
Nice quads. What it's the first time you met dependent type?

>>58247784
It's the first time
no it isn't actually

it's the _th time i've seen such an ugly language

>>58247796
Coq is fucking hot.

>>58247817
Stop lying.

>>58247927
We don't share the same taste anon.

>>58247973
My taste is right

Do any of you use functional programming professionally (i.e. get paid* for it)? I'm studying Scala** with the hope that it might get me out of enterprise code-monkey hell.

* Grad student stipends don't count.
** I know it's shit.

>>58248209
If I sit around at work and hack away with Haskell, I guess you could say that I'm getting paid to write it...

>>58248209
Yes.

Is there anyone else who does nothing but implement toy languages?

>>58248375
Bjarne Stroustrop

>>58248375
Me

File: dependently typed.png (5KB, 180x259px) Image search: [Google]

5KB, 180x259px

>>58248375
I want to but I'm no good at it
The best I got was a broken dependently typed language

>>58248754
I didn't say I was any good at it either...

>>58248724
I seem to be making a postfix shell at the moment.

The entire interpreter is essentially

foldM eval

I don't know if this is a good thing or a bad thing.

File: simple typed eg2.png (31KB, 721x377px) Image search: [Google]

31KB, 721x377px

>>58248826
oh i made this, this was alright

My toy language is going to be [spoiler]object oriented without first class functions[/spoiler]

File: 1482687438691.png (258KB, 692x648px) Image search: [Google]

258KB, 692x648px

>>58248863

How to write highly-efficient Haskell code?

>>58249008
Use unboxed types everywhere

>>58249008

! ! ! !! ! ! !! !!!Vector ! !! {-# UNPACK #-}!! ! ! ! !

>>58249058
>!!
>(!!) :: [a] -> Int -> a
don't do this!

>>58249109

$! `seq` `seq` `seq` $!! ByteString `deepSeq` !!!! -XStrict !!!!!

>>58248879
However, I could create syntax sugar that generates objects with an apply() method. If you think about it, it'd be just about as functional as common lisp

>>58249008

{-# LANGUAGE Strict #-}

laziness is not good
fite me

>>58245347

post = "R" ++ repeat 'E'

Where do I find specifically where a function is in a module?

I am doing some gtk things with the graphics.ui.gtk module, and I prefer to explicitly import each function from where they live, so instead of just

import Graphics.UI.Gtk (mainGUI)

I'd prefer to have

import Graphics.UI.Gtk.General.General (mainGUI)

Now, I know where this one lives, but how can I quickly find where all the other functions in submodules are?

>>58249842

λ import Graphics.UI.Gtk
λ :info mainGUI
mainGUI :: IO ()     -- Defined in ‘Graphics.UI.Gtk.General.General’

File: 6.png (209KB, 3757x2411px) Image search: [Google]

209KB, 3757x2411px

>>58249865
Thanks friendo

With linear types, there are two kinds of conjunctions. The first is the multiplicative A*B, where you can project out both A and B like a normal pair. The second is the additive A&B, where you can only project out either the A or the B.

Record syntax {A, B, C, ...} is equivalent to A*B*C*..., pretty intuitive, but I would like to augment the syntax to allow certain fields to be mutually exclusive like with &. Because the records are to compile to structs, preserving order, I also don't want the syntax to force you to group the mutually exclusive fields. How do you think I can best express this in the syntax?

>>58250736
you should probably have different record syntax for each, but you can still "compose" them in the usual way;
{a::A,b::B,cd::[c::C|d::D]}
or visa versa
[a::A|b::B|cd::{c::C,d::D}]

what's the syntax you have in mind for committing to a particular linear field?

>>58251339
The issue with that is that it limits what you can do with the struct layout.

>what's the syntax you have in mind for committing to a particular linear field?
Just x.y.

>>58250736
>The second is the additive A&B, where you can only project out either the A or the B.
How is this different from a linear value of type Either a b?

>>58251481
With A&B the choice is made when it's eliminated, but with A+B the choice is made when it's constructed.

>>58251373
Why would the syntax limit the compiled implementation? Could the compiler notice "this is a linear product embedded in another product, INLINE ALL THE THINGS"?

>>58251590
Let's say I want the struct to be laid out like {A, B, C} but I want the A and the C to be mutually exclusive.

>>58245612
haskell: orange
Lisp: black

>>58251508
Oh, of course. Thanks.

>>58251649
That seems like an awkward way to actually code; the 'grouped together things' are not located syntacitcally near each other, but whatever.

how about making it look kinda like a typeclass constraint:

(A&C) => {A,B,C}

>>58245612
CL: light blue
Racket: Red
Haskell: Red
Perl: Yellow
C: Gray
C++: Dark blue

>>58244769
I just Passed my Java Programing Class with an A and i barely know how to even code properly

>>58249449

post = 'R':['E','E'..]

>>58252970

codata Stream (A : Type) : Type where
  head : Stream A => A
  tail : Stream A => Stream A

post : Stream Char
head post = 'R'
head (tail post) = 'E'
tail (tail post) = tail post

>>58252996
>>58252996

#lang racket
(define post
  (for/stream ([i (in-naturals)])
    (if (zero? i) #\R #\E)))
(stream-for-each display post)

>>58252970
>>58252996

post :: String
post = s (s (s k k) (k 'R')) (s (k y) (s (s k k) (k 'E'))) (:)
  where s = ap
        k = const
        y = fix

>>58252970

post = 'R':'E':tail post

>>58253163
slightly improved by moving all of the literals to the end

post = s (k (s (s (k s) k s (s (k s) k (s (s k k)) k)))) (s (k k) (s (k (s (k y))) (s (k s) k (s (s k k)) k))) 'E' 'R' (:)

>>58253294
Can't you express y in terms of s and k?

>>58253324
Not in Haskell, because it requires constructing an infinite type

(Although you can embed infinite types using a newtype wrapper, that would be uglier than just defining y as an extra primitive)

I'm currently doing the intermediate section of the wikibook in the OP on Haskell and I still have no idea how I would build a proper program yet, just regular functions

Functional programming is useless and gay.

http://flyingfrogblog.blogspot.no/2010/08/parallel-generic-quicksort-in-haskell.html

>>58253271

post = 'R' : repeat 'E'

>>58255372
What part confuses you?

>>58255542
Sure I can make functions to operate on lists and generate data but what's the point if I can't do anything with it. I guess it only just introduced actions and the IO stuff but I don't really understand how it works. If it's just a function that returns a value then how does it output to the console.

I'll keep going through it. It's probably just my imperative plagued ways of thinking that are getting in the way

>>58255565

myFunction x = x + 10

main = do
    print (myFunction 5)

It's that easy. Don't listen to the 'hurr, Haskell has no I/O' imperatards.

>>58255565
You normally use monads.

In a way, it's sort of like you're building up an AST describing what to do.
You use lambdas to say "given this result, do this"

>>58255626
Fair enough

>>58255633
Monads haven't come up in the book yet. I'll keep them in mind

>>58255565
>>58255633

I had a good example for something but I can't find it.
So another way of doing this, that would be much more limited, would be like this:

data Instruction = Add | Count | Switch | Push | Pop | Print

You can then describe programs as a list of instructions

type Program = [Instruction]

And write code to execute it

run :: Int -> Int -> [Int] -> [Instruction] -> IO ()

in this example, it's a simple (2 register + stack) machine, and you can't branch or return arbitrary types, you can only sequence

>>58255690
Found it

https://archive.rebeccablacktech.com/g/thread/S58009006#p58009536

There's actually a much simpler embedding, which is to encode the instructions as (MachineState -> MachineState) functions, then you can simply compose then using (.) rather than lists. (And just execute them extremely simply)

>>58248209
I work professionally in Scala. It's good but you will still suffer enterprise bull shit though you will get a higher salary for it.

>>58255730
That's essentially Joy.

Anybody with thoughts on Elm?

What are some good projects to get used to Haskell as someone who has just learnt some?

>>58256827
Command line calculator

Does logic programming belong to functional programming?

>>58257050
the correct answer is "ehhh"

>>58257050
>>58257054
but with that said, you are more likely to be welcome here

>>58257050
No, but nowhere else will take you either, so you might as well stay here.

>>58255626
that ‘do’ is redundant

main = print $ myFunction 5

>>58257767
main = (do print) (do (do myFunction) 5)

>>58256847
Not him, but trying that right now. How do I take a list as user input?

>>58258730
There a few ways

One is extremely straightforward - just use readLn

[34, 23, 754, 23, 43, 53]

this is how the read instance for lists works

otherwise, you could have
34 23 754 23 43 53

and do (map read . words)

>>58258730
>>58259002
and if you want to do some more unique stuff, you can use parsec

>>58244837
Lisp has many functional dialects.

>>58259844
>>>>>>>>>>>>>>>>>>>>>>>>

>>58244860
>purely functional language
Best feature.

My day job is on a Javascript compiler, and we can't optimize the function foo(x) { var dead = x+1; return x; } because x might be an object whose valueOf has side effects.

>>58261290
>Javascript compiler
Why would people ever need this?

>>58261290
AAAAAAAAAAHAHAHAHAHAAAAA

>>58261785
HAAAAHAHAHAHAHAHAHAHAHAHAHAHA

>>58262437
For real, why?

>>58263632
If I could think of a single valid reason for compiling JavaScript the idea wouldn't be nearly as funny.

File: 1482242138570.jpg (122KB, 600x600px) Image search: [Google]

122KB, 600x600px

>tfw your school teaches scheme to first year CS students
>tfw you're in the software engineering program so they teach you C instead
feels bad man

what's the easiest first functional programming language to learn? Should I read SICP?

File: alternating sequences.png (17KB, 540x286px) Image search: [Google]

17KB, 540x286px

Type safe alternating sequences

So, I was programming in Haskell and I wanted to take the chance to learn about Monads, but never ended up using them.

How useful are Monads and how often do you use them?

>>58257050
declarative programming general??
>>58266179
if you're in Haskell, like literally everywhere

>>58265390
Wow this could revolutionize data streaming forever

Patent this NOW my friend