/dpt/ - Daily Programming Thread

old thread: Hello, are you making a nice code?

Other urls found in this thread:

codeproject.com/articles/528178/load-dll-from-embedded-resource)
jekyllrb.com
w3schools.com/howto/howto_html_include.asp
twitter.com/SFWRedditGifs

First for C

Java is good

i am making rude code and there is nothing you can do to stop me

You didn't use usual OP, please keep them consistent.
also your janny ebin

>people actually think Scala has dependent types
Screaming

Kan dere være så snill å skrive på norsk? Dette er et norsk tråd.

trying to make a rock, paper, scissors game in java with a GUI. just going through pseudocode right now, any advice?

don't use java

faen ass, nå må du gi deg!

is it swing? I hope it's not swing. That would be my advise. Don't use swing.

>pseudocode
Why do people do this?
It's completely pointless.

It can be helpful when the final code must be written in an extremely verbose language such as Java.

>dependent types

?

>people actually think it doesn't

i'm still new to programming in general, i'd like to hear some more of what you guys think though.

Unfortunately I have to use java, it's for an assignment @ uni

Γ, x:A ⊢ B:Type
――――――――――――――――
Γ ⊢ Π(x:A)B:Type


Feel free to go ahead and show value dependency in Scala's type system.

have you heard of the word monad before?

>gibberish

The fuck are you going on about faggot?

nope, what's monad?

It's just busywork garbage taught at universities.
It's equally as worthless as using UML diagrams.

Schools still teach UML unironically, they become completely unreadable as soon as you start planning programs with more than 5 functions.

I would Google "dependent type" and copy paste some paragraphs from Wikipedia but you can do that yourself.

linus...

I think you mean

>Scala doesn't have this particular subset of dependent types

>In computer science and logic, a dependent type is a type whose definition depends on a value.
>not just calling it value-dependent types

computer scientists really do suck at naming things

It's useful if you're a pleb and can't stop yourself from using inheritance. Inheritance basically requires you to know all your classes and their relationships ahead of time or you will waste a lot of effort on going over your old code and refactoring it constantly when adding a feature that requires a new class.

no, he meant
>scala doesn't have dependent types

trait Wotsit {
type A
}

def bozzer(w: Wotsit)(implicit m: Monoid[w.A]): w.A = m.zero

What is the hardest to master high level programming language?
Is it Haskell?

C++

People say it has "path-dependent types" but I've seen no evidence that it's anything that's not possible with GADTs.

Value depending on value - function
Type depending on type - type family
Value depending on type - overload
So there's no reason to prefix "dependent" with "value-".

How is this different from:
def bozzer[A](implicit m: Monoid[A]): A = m.zero

You're going to need a better example than that.

>there's no reason to prefix "dependent" with "value-".

yeah I see you enjoy being impenetrably terse. no wonder 90% of every academic writing reads like shit.

Should I learn Rust or Idris next? I want to give both a go eventually.

Pseudocode, yes or no?

gay

I say yes.

As i'm writing code I like to have a notebook next to me, so I can keep track of what i want to do or what I think the computer is doing. I never erase anything, and I never throw out my papers

rust

...

Ah, yes, I had almost forgotten about that piece of software.

I'm trying to embed sfml.net dlls into the exe file. According to the sfml website, "sfml.net is built on top of the C binding (csfml)", so it has some dlls in c# and others in c, I think.
I was able to easily embed some of the dlls using Costura.Fody, but embedding csfml dlls simply doesn't work.
I've tried other methods too (like codeproject.com/articles/528178/load-dll-from-embedded-resource) but it says the dll should have a manifest or something.

A monad is just a monoid in the category of endofunctors, what's the issue?

formal pseudocode, no not really
description of procedure in chunks of steps, yes.

Formal pseudocode is for like explaining algorithms on wikipedia, the other one is for giving yourself/ a team an idea of what happens start to finish (like take item out of fridge, use item in meal, wrap meal, store in freezer for later use).

If you can write something into pseudocode you pretty much wrote it for real.

Use javafx, or even make it a webapp. Just dont use swing

>user posts an easily-debunked "example" for how Scala has dependent types and then fucks off when challenged to post a better one
Really makes you think.

Does html have a #include tag of some sorts?

I want to make a pure html static website without dependencies on tools such as template engines but I can't figure out a good way to put something such as a page footer on a separate file and include it in every page.

HTML imports make no sense, is dynamic. The closest thing to what I want seems to be , and even .

How could HTML be this fucked up? This is literally 80s technology

So, what, a dependent type is a type that can be something else? I've never really understood that shit.

no

>Does html have a #include tag of some sorts?
yeah, it's called Ctrl+c, Ctrl+v

javascript can include html pages for you though

And a monoid is just a monad in the category of endofunctors. It's beautifully symmetric.

I want my pages to work without javascript.

Really?

Template engine or bust, dipshit

dragging my poor old under-caffeinated brain through writing a web application in Perl because it's the best programming language for web applications (ok, it's the only one I know. it's been ages since I wrote a web application)

user OOP might be a zero overhead model in the mind of the crazies that use it but the fact of the matter is that it doesn't boil down to that in a compiler.
Sure. With a perfect compiler you'd be right. The exceptions are the issues.
But there's more to it in the real world.

And if we look at the low level situation of today I simply don't see how the programmer can reach the level of specificity that would be required to make a program go fast in a realistic scenario. You have to remember that the more potential you leave open the less the compiler can do. Using volatile variables just kills optimizations. Aliasing kills optimizations. Virtual functions (dynamic dispatch in general, but virtual functions in particular) kill optimization. If we had a more flexible OOP programming language than C++, which is very limited in its inheritance model in particular, you'd only increase these issues.

So you're absolutely correct and wrong at the same time. When I hear low level programming I'm assuming a real world scenario, with all considerations you can have. And compliers are just software. They're not magic.
>a good chunk of performance critical...
Yes. But while I haven't looked at your examples I can confidently say it's not gonna be pure OOP down at those high performance parts of the code. That's what user requested. He wanted OOP and he wanted to be 'the best' at high performance software while using OOP.
You often find that they move away from C++ as they need more performance. An example would be Mike Acton's 2014 Cpp con talk. It gives a nice view of the rules they have for their games and surrounding tools.
Question actually comes up why they use C++ and the answer is obviously that they'd rather use lower level languages like asm or C. But there's not enough hires to make that feasible.

OOP is in direct opposition to high performance right now. It doesn't abstract in a way that gives Compilers more power/opportunity.

It's very helpful. It's a planning step where you don't consider it supreme to your experience.

>I don't want to use server smarts
>I don't want to use client smarts
>waaah why is html not smart

You may be suffering from retardation.

No, it isn't Haskell.
You asked this before.

if you don't want to use js or a basic cms with a template engine, write a set of scripts that will generate static HTML pages from source and template files. i can't remember the name, but there's some hyper-minimalist blogging platform where you have to manually run a program to generate all the html every time you make a new post.

really neat function for python, I stole the first function from stafck overflow, but added the rest of the code to move around like a rougelike, cept its not going to be a rougelike, gonna be a text based rpg, but with map movement

import os, sys, tty, termios

def key_pressed(char_width=1):
fd = sys.stdin.fileno()
old_settings = termios.tcgetattr(fd)
try:
tty.setraw(sys.stdin.fileno())
ch = sys.stdin.read(char_width)
finally:
termios.tcsetattr(fd, termios.TCSADRAIN, old_settings)
return ch

def print_board():
for row in range(45):
for col in range(35):
token = board[row][col]
if not token:
token = " "
print(token,end=" ")
print()

board = []

for row_num in range(45):
row = []
for col_num in range(35):
row.append(" . ")
board.append(row)


player = " @ "
empty = " . "


old_row = 0
old_col = 0
current_row = 0
current_col = 0


playing = True
while playing == True:
print("\n"*75)

board[old_row].pop(old_col) and board[old_row].insert(old_col,empty)
board[current_row].pop(current_col) and board[current_row].insert(current_col,player)


print_board()


kp = key_pressed()

old_row,old_col, = current_row,current_col

if kp == "j" or kp == "s":
current_row +=1
if kp == "k" or kp == "w":
current_row -=1
if kp == "h" or kp == "a":
current_col -=1
if kp == "l" or kp == "d":
current_col +=1

decimal : Bool -> Type
decimal True = Float
decimal False = Int

value : (b : Bool) -> decimal b
value True = 1.5
value False = 1

It's a type that depends on a value.

Think of an array. You have the type of the elements as well as a length. To index this array without the possibility of an error, you need an index that is less than the length. While you can do this just fine without dependent types, dependent types allow this length to be determined dynamically even though the types are static. While it's easy to see how you get an array of that length (by construction), it can be trickier to see how you get an index. One way is to enumerate all the indices from 0 to length-1, like with a for loop. Another way is to take an arbitrary natural number (unsigned integer) and check that it is less than the length.

It all works out because of immutability. The "value" only exists in the type as a placeholder. You can still operate on placeholders, though, by using identities such as x+y = y+x. If you have a value of the type "indices less than (x+y)", you can use it to index a value of the type "arrays of length (y+x)" by first coercing it using that identity (or you could coerce the array), which is a no-op at run time (unless you're in homotopy type theory, but that's another tale for another time).

jekyllrb.com

Yeah fuck you too.

Why is HTML unable to do something simple such as ? You just take that node and replace it with whatever elements are being included. Why does it need a goddamn external tool to do that, complete with its own idiotic hipster language you gotta buy into?

If anyone's retarded here, its the folks who have been standardizing HTML and still haven't added this simple feature in.

>write a set of scripts that will generate static HTML pages from source and template files.

Actually that's my current situation. I would prefer to write everything in HTML5 without any of these scripts if I could avoid all the stupid repetition.

Specifically, it's the value depended on that's immutable. There's no way to update that length so that the types are inconsistent even though they depend on the same value. If that makes any sense. Modelling a destructive update as a new variable binding that shadows the old one is one way to do that.

If you had something like:
length = readUnsignedInteger();
array = newArray(length);
length += 1;
index = makeValidIndexLessThan(length);

what the types see is:
length = readUnsignedInteger();
array = newArray(length);
length2 += 1;
index = makeValidIndexLessThan(length2);

'index' depends on 'length2' and 'array' depends on 'length' so they are not innately compatible. But there may be an identity you can use to make them so when it is valid.

So it's... a hybrid of static and dynamic types? You put the bounds checking code into the type system and call it dependent types?

>>I don't want to use client smarts
w3schools.com/howto/howto_html_include.asp

No, not at all. There is somewhat of a relation to dynamic/static, where dependent types make it possible to make more information that is traditionally only dynamic, static.

In a fully dynamic system, both the type of elements of the array and the length of the array would be dynamic. In a more static system, the type of the elements could be static, but the length would have to remain dynamic. Dependent types allow you to make it all static.

A friendly advice.

C and Racket are probably not the languages that will land you more jobs. But are the ones that will teach you the most. Learn them if you can.

I personally like python a lot, haskell is also good. Sup Forums memes a lot about the last one and that is what monads are about.

How is dynamic information made static when the type is only determined at runtime where values actually exist?

The type system allows you to make a type depend on a value, whether that is at runtime or compile time is completely incidental (some languages don't even have a compile time).

logic
you have to prove your code to the compiler

>they don't even try to search it
Retards the lot of them. Thanks for your generosity user.

though in simple cases, e.g. , it can just analyse the cases

what are you thanking him for exactly? did you look at the full example?

>allows you to make a type depend on a value
Ahhh, I gotcha.

... you actually think that is a good solution?

Like I said in , the type system doesn't know what the value exactly is if it's determined dynamically, it uses a placeholder (free variable). But it knows about relationships between these placeholders and symbolic computation is possible.

I was thinking of bloxsom because muh perl

bloxsom can run either as a dynamic CGI script or it can generate a complete static HTML site. Is there any reason you don't want to use a server-side solution though? There are some very simple/powerful/flexible template engines that serve "static" HTML that was generated on the fly by the server.

>good solution
It's web. It's good enough. You get the convenience.

so for instance, C++'s std::array
except because it's logically proven (that it works for ANY t or n)
both T and N can be decided at runtime

you said
>I want my pages to work without javascript.

This sounds a lot like the constraint analysis optimizers do on code

if (x > 10) {
// type of x kind of becomes "int > 10"
} else {
// type of x kind of becomes "int

>good enough
>needs JS to even load the page

Honestly, I didn't fully understand dependent types until I programmed my own type checker for a simple dependently-typed lambda calculus, and I had to learn about reduction, normal/neutral forms, etc.

They are very closely related.

How about you just write your own God damned preprocessor? Like any moderately ok programmer would have done already instead of complaining.

This is something a dependent system might use, but not for constant optimisation.

Refinement types are a limited subset of dependent types, and refinement types are like this:

type T = { x : int | x < 15 }
T value = 16; // error

if only there was already some kind of .... Hypertext Preprocessor... Maybe with a recursive acronym, since all good projects have recursive acronyms...

Well because every templating engine sucks. They're all quirky in their own ways and just make me waste time learning them and working around their stuff. It's also a dependency that really shouldn't be necessary.

I just want to write pure HTML5 content. I have a lot of metadata encoded in pages using microformats and templating engines and their ridiculous languages basically make me revert back to XML for those anyway.

It's still better than stupid shit like PHP though. HTML should be served by the web server. If I need dynamic content, I'll have the page ask an API endpoint for it via Javascript.

I already did. Had you actually read the post, you'd have realized that's not what I want.

Why bother finding one it's just a single token parser and three fprintf's and an fopen.

>without dependencies
It's a static website. When it's done it's done.

Actually, a compiler for a dependently typed language could do a lot of optimizations with the information it gets. Or, rather, the redundant checks don't need to exist in the first place for the same reasons that they can be optimized out.

A dependently typed language can be compiled and optimized very quickly, assuming you don't expect much in the way of type inference (which involves hard problems like unification and satisfiability - optimizers for less richly-typed languages have to do this themselves).

You're a fucking idiot m8.

no u

>A dependently typed language can be compiled and optimized very quickly
...unless the type signature forms an infinite loop

>Actually, a compiler for a dependently typed language could do a lot of optimizations with the information it gets. Or, rather, the redundant checks don't need to exist in the first place for the same reasons that they can be optimized out.
That's what I mean.
It's partial application of stuff that's known at compile time.

That comes from purity

>Why does it need a goddamn external tool to do that
It doesn't. HTML5 can do that by itself.

PS: Javascript is part of the HTML5 spec.

>Javascript is part of the HTML5 spec.

It can also be disabled.

I have used several different perl web templating modules over the years and in their most basic forms, none of them were more complicated than:

or
['footer']
or even

but I'm sure that last one was way too fucking complicated of a hipster language for you. get fucked, idiot.

On that note, refinement types are precisely those dependent types for which unification/satisfiability is decidable. E.g. an array of length (x+0) will automatically check as an array of length x because x+0=x is a formula in Presburger arithmetic, which is decidable.

Which is what totality is for.

Well, constant folding only requires purity and totality. Dependently typed languages are a good place to find those, for sure, and such a language could certainly have a way to fold expressions containing free variables (which is usually hard) given identity proofs.

>imperative users will never know of the indexed state monad
>dynamifags will never know of the indexed state monad

>they will never understand the magic of statically checked type changing variables

Yeah fuck you too dickface

Linear types admit strong update, too.