>Lisp girl Please use a functional programming related anime image next time
Isaac Richardson
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.
Joshua James
Homotopy type theory is always presented as Martin-Loef type theory, not as a pure type system.
Hunter Turner
Hott is an extension of MLTT. whats your point even?
Asher Stewart
>Maki >ever Karen best girl. Exactly this picture made me create the first /fpt/ ever.
t. Creator, splitter and autist OP
Matthew Ortiz
Maki is holding the HoTT book but has a CoC overlay.
Landon Howard
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.
Levi Diaz
So would it be more accurate to say that FP really needs some mechanism of partial application? That applies to both lambdas and combinators.
Ethan Price
I thought you might be confusing closures with some other concept.
Sebastian Gutierrez
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.
Nolan Lewis
I'm a different poster, I'm relating this back to .
Jaxson Phillips
Yeah, well you know what? I made that image, so I made you who you are
Levi Bennett
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).
Logan Sullivan
>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
Tyler Rodriguez
post = "R" e where e = "E" e
Elijah Harris
>no Higher Order Perl
Jordan Harris
>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.
Austin Gray
>>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.
Sebastian Bennett
>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?
Ayden Peterson
Who is it?
Dylan Peterson
Yes >its extraciricular meaning it wont count for credits Who the hell cares.
Jonathan Scott
Yes. It's useful. You can always tell employers you know it.
Brayden Lee
I want to go
Adam Hernandez
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
Ryan Brown
Haskell: Red and White
Matthew Bell
Haskell is violet, F-Sharp is blue. Happy New Year, user, I love you!
Liam Johnson
> () is string concatenation > () is not an inequality check your language a gay that's just the logos nerd
Dylan Sanders
Functional poorgramming is a joke.
Ian Sanders
Lisp is yellow, Haskell is blue (and grey and purple to lesser extents), OCaml I try not to think about.
Benjamin Myers
> () is string concatenation Oh dear, user, you have a long way to go.
Hunter Sullivan
She just told you she loves you and you call her a nerd?
Blake Carter
() is just any binary associative operation on algebraic objects with a monoidal structure.
Charles Gonzalez
/= is best inequality. Go back to shitcaml you scrublord
Isaac Cook
Thanks OP for adding the second Haskell book. I've been trying to find it.
Joshua Fisher
>not using FiraCode so != looks like ≠
Carson Morris
What the hell is a FiraCode and why aren't you using emacs where you can configure anything to look like arbitrary unicode symbols?
Jayden Gomez
...
Colton Anderson
a font
baka
Tyler Hall
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?
Camden Flores
Language?
Logan Foster
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') }
Sebastian Cook
What are you going to use to implement it?
William Smith
Probably Haskell.
Jack Bailey
Yeeeeeahhbuddy.
Matthew Barnes
Is it understandable enough? It uses self typing (x : F x) and sized types for termination checking but otherwise it's pretty standard.
Christian Price
sounds like a gay language, just use (++) for that
David Martinez
Trolled hard.
Wyatt Gonzalez
it seems pretty weird at first glance. like what is $i and #? I do like the pattern matching syntax a lot though
Logan Bennett
That's taken from the MiniAgda sized types syntax. $ is successor and # is infinity. arxiv.org/pdf/1012.4896
Nathaniel Phillips
Haskell: Green Lisp: Yellow OCaml, F#: Orange Erlang: Red - C: Black
Ryan Harris
whatever happened to lainchan?
Colton Perez
It's alive, and very, very*, slow.
*very
John Wright
The Haskell thread is dead
Luis Collins
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.
Aiden Kelly
Name a dependently typed language with at least mediocre performance.
I'll wait.
Sebastian Sullivan
You can compile the rooster to caml if you want. So performance is not a problem.
Ryder Carter
ATS
Tyler Kelly
>You can compile to caml so performance is not a problem
Mason Collins
interesting. IMO the syntax is a bit too terse in that case, but idk how to make it more descriptive without making it Java literally faster than any other FP language Ur, ATS, F* possibly
Easton Morris
>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.
Angel Adams
Let me show you my dear blonde user: 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.
Ryan Rogers
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.
Hudson Hall
ew
Adrian James
Nice quads. What it's the first time you met dependent type?
Justin Scott
It's the first time no it isn't actually
it's the _th time i've seen such an ugly language
Jaxson Long
Coq is fucking hot.
Jack Murphy
Stop lying.
Jaxson Moore
We don't share the same taste user.
Carter Kelly
My taste is right
Angel Morris
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.
Christian Johnson
If I sit around at work and hack away with Haskell, I guess you could say that I'm getting paid to write it...
Michael Richardson
Yes.
Christian Watson
Is there anyone else who does nothing but implement toy languages?
Jacob Price
Bjarne Stroustrop
Carson Russell
Me
Thomas Foster
I want to but I'm no good at it The best I got was a broken dependently typed language
Isaiah Allen
I didn't say I was any good at it either...
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.
Colton Gonzalez
oh i made this, this was alright
Dominic Scott
My toy language is going to be [spoiler]object oriented without first class functions[/spoiler]
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
Grayson Williams
{-# LANGUAGE Strict #-}
Connor Long
laziness is not good fite me
Cooper Hughes
post = "R" ++ repeat 'E'
John Thompson
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?
Ian Morales
λ import Graphics.UI.Gtk λ :info mainGUI mainGUI :: IO () -- Defined in ‘Graphics.UI.Gtk.General.General’
Gavin Walker
Thanks friendo
Jackson Gonzalez
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?
Nicholas Ward
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?
Carson Nguyen
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.
Henry Harris
>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?
Gabriel Perez
With A&B the choice is made when it's eliminated, but with A+B the choice is made when it's constructed.
Leo White
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"?
Dominic Phillips
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.
