/dpt/ - Daily Programming Thread

old thread: What are you working on, Sup Forums?

Other urls found in this thread:

github.com/rust-lang/rust/pull/36016
github.com/EnriqueB/FunctionFinder
idris-lang.org/
github.com/deeepaaa/rana
incredible.pm/
elm-lang.org/examples/random
twitter.com/SFWRedditVideos

bump

first for python

Repostan:

They're already in nightly: github.com/rust-lang/rust/pull/36016

Example:

#![feature(untagged_unions)]

union Foo {
x: u64,
y: (u32, u32),
}

fn main() {
let f = Foo {x:1};

println!("{}", unsafe{f.x});
println!("{:?}", unsafe{f.y});
}

Output:

1
(1, 0)

n-th for meme programmers ITT

static const char const *const arr[] = { "poop", "dick" };

This is valid C.

There are much worse examples of valid C than this. This is actually legible (although highly redundant)

New Jade/Pug-like (but lightweight) template engine for js.
Started after it turned out that compiled jade templates occupy more RAM (about 14 GB) than all the other site content combined.

Custom iterator in C++14.

You?

any of you niggers know a good movie with programming in it?

Blood-C: The Last Dark

>Idris vectors are completely unoptimised linked lists

>It's probably the case that countyBox.SelectedItem is null, probably because it doesn't have a meaningful value? (i.e. nothing selected, or multiple items selected?)
I think so. I think that when I'm switching to another state, it's still firing the SelectionChanged event and at that moment, the selected item for countyBox.SelectedItem is null which is casuing it to throw nullref in the first place. Back to the shitting street for now.

Hey I've tried vim but I don't type on home row and don't use the keybindings very much. Whats a good graphical text editor that's available on Arch? The closest I've come is Kate but it has wierd issues with its file manager plugin that I don't like.

I've just been using nano with terminal tabs but I'd like syntax highlighting, a filetree preview so I can see my programs file structure and like auto tabbing and automatic bracket closing.

...

It is.

Just add a city.SelectionClear() to the selection changed on the State dropdown, or handle the potential null value at the beginning of SelectionChanged on the city.

>anime

no thanks buddy

Sounds retarded

Church/Scott encodings are so cool.
Bottom : Type
Bottom = (A : Type) -> A

Unit : Type
Unit = (A : Type) -> A -> A

Boolean : Type
Boolean =


Yeah, it's kind of silly. Stronger types allow you to get rid of redundant runtime checks and retain safety, but it doesn't matter if you're losing performance in other, bigger areas.

>he doesn't watch Ghost in the Shell

You're absolute cancer.

I've already seen it, meanie

nano has syntax highlighting, filetree preview, and autotabbing

>automatic bracket closing
you don't need that

finished up my type inference engine
about to write a code generator

Currently working on a recursive solution to the Eight queens problem, but am running into a small problem:

Given an object, how could one copy it and, after changing the first object, set it equal to the second (copy) object.

I guess what I'm asking is, how would it be possible to do this:
void foo(int bar)
{
int barCopy = bar;
/*
Manipulate bar
*/

bar = barCopy;
}


but with objects (I have a chessGrid object that I'm manipulating, but am having a hard time unmarking the board once I remove a queen)

I built a genetic programming system in C++ that finds a function that approximates a series of points.

Theres lots of room for improvement and further work (such as functions with multiple variables and more operators). I will continue working on this.

How did I do, Sup Forums?

github.com/EnriqueB/FunctionFinder

Oops, forgot to finish my thought.
Bottom : Type
Bottom = (A : Type) -> A

Unit : Type
Unit = (A : Type) -> A -> A
unit : Unit
unit _ a = a

Boolean : Type
Boolean = (A : Type) -> A -> A -> A
true : Boolean
true _ a _ = a
false : Boolean
false _ _ a = a

Natural : Type
Natural = (A : Type) -> A -> (A -> A) -> A
zero : Natural
zero _ a _ = a
succ : Natural -> Natural
succ m A a f = f (m A a f)

Recovering induction instead of just recursion using Self types is neat, too. Not sure how sound they are, though.

I'm making a 3D engine from scratch.

Set up the DXframework, vertex and pixel shaders today, and managed to render a triangle. May not sound like much, but man was it a hassle.

Feels great now though.

if you're still here, the solution is
digitSum x = x mod 9

> (I have a chessGrid object that I'm manipulating, but am having a hard time unmarking the board once I remove a queen)

do something like
board.set(x,y)
result = recur(board)
if (result == fail) {
board.unset(x, y)
}

Alright I'll read the docs better for nano and setup my conf then.

If you are already doing it recursively, you can just let the stack do it for you (you dont really need a custom type for this problem).

If you dont want to do that, you can do this, IIRC:

void foo (custom_type bar){
custom_type copy = bar;
//do stuff to A
A = bar;
}


That should work unless you do some dynamic memory stuff inside the custom type

i think the idea is that you would write out your system in idris and generate safe code from that, if you want performance

woops, messed up the code
void foo (custom_type bar){
custom_type copy = bar;
//do stuff to bar
bar = copy;
}

>Idris is a general purpose pure functional programming language with dependent types.
idris-lang.org/

There are already lots of dedicated proof assistants for formalizing code that is written in another language.

Yeah, I'm doing a dynamic memory allocation (to get different sized arrays so it can later work with more than 8x8 grids), so that might be part of the issue (?)

Here's some of my sample code for the recursive backtracking:
chessGrid tempGrid = currentGrid;
Queen tempQueen(rowNum, col);
markGrid(currentGrid, tempQueen);
std::cout

i thought that was what idris was
maybe they got fooled by memes saying it was general purpose

i already showed you how to do this in also you don't need to store the whole grid, you can just store a list of queens tested so far,
that's up to you though

github.com/deeepaaa/rana

not yet complete but i'm lazy

forgot to attach a picture...

Here is a sample run of the system trying to find the function
y = x*(x+5)

You got fooled by whatever it was that made you think Idris was just another proof assistant.

nope, i'll admit i never really knew in the first place

If you are using dynamic memory then you will need to code a copy constructor for your class, which I don't really remember how to do...

Try looking in google for some sample code, they are not hard to code

Yeah... Admittedly, I'm still a pretty inexperienced (read: bad) programmer, and I was trying to make things work my way when they probably wouldn't

But your solution sounds way better. Thanks! I appreciate the help!

do you actually think this is a good idea?
lol
this is the most pajeet thing ever

>Using the propositions--as--types correspondence, abstract data types can be identified with logical theories, and proofs of the theories are the objects that inhabit the corresponding ADT.
Huh.

what a spiteful reply

>Huh.
What do you mean by this?

It really makes you think...

actually i feel kinda bad for saying that
but what's the point of making it look like c when it's not c

Removing thread leaks and adding update feed pooling for a realtime shitposting engine. Working on unit tests at the moment.

It really does make me think - can you do the reverse? Can you take an arbitrary logical theory and encode it as an ADT?

#include
#include

void str_rev(char *dest, size_t size, const char *str)
{
int buf_idx = 0;
char *new = str + size; //no warnings pls
while(new-- > str) {
dest[buf_idx] = *new;
buf_idx++;
}
dest[buf_idx] = '\0';
}

int main(int argc, char *argv[])
{
if (argc != 2) return 1;
int len = strlen(argv[1]);
char buf[len+1];
str_rev(buf, len, argv[1]);
printf("%s\n", buf);
return 0;
}


hello this code snippet seems pajeety
could someone give me a few pointers to improve

yes, quite easily

i'd personally rather see something like "}}}}" than

Yeah, never mind, the answer is obvious. Not quite an Archimedes moment.

a ^ b = (a, b)
a v b = a | b
a -> b = a -> b

wait I might've used the wrong symbols

I meant
a and b = (a, b)
a or b = (a | b)
a implies b = a -> b

if (argc != 2)
returns when i supply two arguments instead of just ignoring the second.

printf("%s\n", buf);
You could just use puts() here.

while(new-- > str) {
I would rather decrement new directly above/below incrementing buf_idx for better readability.

That's just reiterating the correspondence. I meant, can you encode an arbitrary theory, e.g. Peano arithmetic, as an ADT?

But now that I think about it, that's just implementing a type of Peano numerals with all of the various operations implemented and laws adhered to.

thanks

Looking for a thing right now to link you but it's fucking hell finding it

Atom.

Also post your programming desktops.

Don't use Atom, Atom sucks. Checkout VS Code

VS Code is shit though.

VS Code is based on Atom...

No, VS Code and Atom both use Electron.

why? Faster than Atom, great plugins.

No, it is not. It just uses Chromium as a base, same as Atom.

Ok, I just found it
Fucking hell that was too much work

incredible.pm/

In my experience it's not faster than atom. I'd say it's slower. Also atom has great plugins too.

Neat.

Pretty sure there is general consensus that VSCode is faster. Search for it.

Plugins yeah, Atom is still more popular AFAIK, and probably has a larger base of plugins.

ratpoison

Also, VS Code is written in a sane language, as opposed to Atom.

I don't care about the consensus, I care about my personal experience. VS Code takes seconds to do things like opening a project folder while on atom most things are instantaneous for me.

>a language that compiles to JavaScript
I prefer the original instead of adding layers on top of it, thanks.

I never worked out how custom or helper blocks worked.

At one point it's pretty explicitly programmy, because you'll get to (A v B) which has a block that pattern matches
(in haskell, it's bimap from bifunctor for Either a b)

pic is: prove that you turn an
Either (A -> B) (A -> C) into an (A -> Either B C)
i.e.prove there is a function
Either (A -> B) (A -> C) -> (A -> Either B C)

which is of course
f x = bimap ($x) ($x)
specialised for Either

in the pic, the block in the middle is a case expression.
it's equivalent to:
\case { Left x -> f x; Right y -> g y } (f is above, g is below)
this is (bimap f g)

forgot pic

Atom isn't written in JS, it's written in CoffeeScript. TypeScript is a lot closer to JS than CS.

> I don't care about the consensus, I care about my personal experience.

Just because you want to believe it doesn't mean it's right. It's okay to change your opinion, you know.

So you just use graphical representation for code.

This.
Now, I know you're full of shit.
And Atom is written in CoffeeScript :^)
But you are missing the point. TS is statically typed. Code that is statically typed is not only less likely to contain bugs, but also faster. If you know even a little bit about V8, you will know JS that is written as if it was statically typed can easily be optimised to be only 5-10 times slower than C++. On the other hand type polymorphic code is easily 50 times slower.

ハスケルちゃん a purest :3

It kills me that there's no good TypeScript+CoffeeScript language yet.

TypeScript+CoffeeScript

Why do you want that? TypeScript is just fine on its own, imo. My favorite laungage actually currently.

Your post gave me a headache.

Yes, it's a graphical representation for typed lambda calculi (mainly simply typed) from which you construct proofs

...

I'm not using it for web development tho. At least not exclusively.

Because what's not to like about CoffeeScript? Statically typed CoffeeScript with be beautiful.

Why?

Fuck off. JS isn't just for web dev.

Learn Calculus of Construction

Theorem thm : forall A B C : Prop, (A -> B) \/ (A -> C) -> A -> B \/ C.
intros A B C H0.
case H0.
auto.
auto.
Qed.

Print thm.

And the code corresponding to your picture.

thm =
fun (A B C : Prop) (H0 : (A -> B) \/ (A -> C)) =>
match H0 with
| or_introl H => fun H1 : A => or_introl (H H1)
| or_intror H => fun H1 : A => or_intror (H H1)
end
: forall A B C : Prop, (A -> B) \/ (A -> C) -> A -> B \/ C

Argument scopes are [type_scope type_scope type_scope _ _]

>Statically typed CoffeeScript
What's wrong with Elm or PureScript?

Atom and VSCode are built on Electron, which is basically a stripped singled instance of the Chromium browser. So no, Atom is not VSCode. But both are web apps that run on Electron

>auto
Learn the meaning of game

>implying you can prove UA in CoC

Too separated from actual JS. The beauty of JS and CS is they compile to very readable JS that is very close to the code you write. It's comfortable to stop using TS or CS at any time and continue developing with the compiled JS code.

bucklescript

>The beauty of TS and CS
fucking typos. Got bad hand tendonitis today. Not easy to type

elm-lang.org/examples/random

that sample in TS+Mobx+react
@observer
class GUI extends React.Component {
@observable val = 0;
render() {
return {this.val} this.val = (Math.random() * 10)|0)}
}
}


I like my mutable state, thank you very much.

You can prove anything that it's provable in CoC.

>people unironically use JS for non-web dev projects
seriously, what in the fucking hell is wrong with you?

>Got bad hand tendonitis today
>JavaScript
Can't make this shit up

Too separated from actual JS i suspect. I bet there's a shit load of gotcha's. OCaml is nothing like JS in terms of how it actually works. CS and TS are extremely close.

Why is that funny?

*slow claps*

*steps out of the shadows*

Heh... not bad, kid. Not bad at all. Your meme, I mean. It's not bad. A good first attempt. It's plenty dank... I can tell it's got some thought behind it...

But memeing isn't all sunshine and rainbows, kid...

JS and JS derivatives, yes.

It's much more common than you think.

Hell, even MS's new Universal Apps can be written in C#/XAML or JS/HTML5 to produce the same product.