/dpt/ - Dependently-typed Programming Thread

Perfection doesn't exi...
data Config = Config
{ configLink :: String
, configHost :: String
, configPort :: Int
, configUser :: String
, configPass :: String
} deriving (Show)

ALL FUCKING FIELD NAMES IN THE RECORD HAVE THE SAME LENGTH NIGGA

yikes

>only deriving Show
Not Eq too?

Just learned lua and i'm surprised at how useful some of the features are.
Does anyone here have any experience with lua?
Any useful tips or things I should lookout for?

std::size_t get_ids_length(
char16_t const* string,
std::size_t size=std::numeric_limits::max()
) {
static constexpr int arity[12] = {2, 2, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2};

if (size == 0) {
return 0;
}

// Wrap-around
char16_t op = *string - 0x2FF0;

if (op > 12) {
return 0;
}

std::size_t length = 1;

for (int i = 0; i < arity[op]; i++) {
std::size_t operand_length;

operand_length = get_ids_length(string + length, size - length);

if (operand_length > 0) {
length += operand_length;
continue;
}

operand_length = get_kanji_length(string + length, size - length);

if (operand_length > 0) {
length += operand_length;
continue;
}

return 0;
}

return length;
}

actually posting code to be alpha dominant

i think its neat

>lua
Does it have dependent types? No? Then I'm afraid it doesn't belong in this thread.

given that vichan is no longer in development, what's the next best imageboard engine?

what are you using it for?

Too much whitespace desu

Sorry but 'perfect' and Haskell records don't match.

Eq doesn't look aesthetically pleasing.
(you're right, it should also derive Eq)

Tinyboard + vichan + infinity + OpenIB

why?
Can't you just cast the variables if you're really concerned about the passed type?

Just learned it for fun. I practiced making scripts for some custom game server.

i only do it for other folk im courteous like that

>why?
this is Dependently-typed Programming Thread
>Can't you just cast the variables if you're really concerned about the passed type?
In a word, no

>Dependently-typed Programming
Oh I thought you were joking. I thought this was daily programming thread

>I thought this was daily programming thread
No. it's circle jerk programming general

FUCK OFF YOU CUNT AND STOP DERAILLING THE THREAD

Dirpa Terp arguing about how Program

think you might be looking for fren

OOPsie did it again

In C how do I copy the value from an int to a float? like copying 10 to make it 10.0
On my program I have: float = int1 / int2; but it becomes 0

Attached: 1470091368477.jpg (960x724, 40K)

sounds lot like reddit stuff it take a hike

float x = (float)x / (float) y;

i know it feels very redutant but thems the breakas

rockstar me on linear logic or linear types.

Attached: 2h77j8.jpg (395x650, 86K)

i know neiher of those words and make less than money you

#humble #hustler

OpenIB has install issues
github.com/OpenIB/OpenIB/issues/289

float thing = myInt
10.0 is redundant. as .0 is no more precise than 10

I tried this before and it'll round itself
I need something like float = 5 / 2 so I can have 2.5 but now I'm thinking that I should copy the 2 and 5 to a float first and then divide them.

what? why don't you just var = 2.5 and then check for type instead of involving arithmetic operations at all?

so float thing = 5 * .5;
????

This is my first microcontroller program for the STM8S105K4 chip. It blinks an LED on/off at 250 Hz rate for every other second.

#include
#include "../stm8s_sdcc.h"

#define LED_PIN 5
#define TIM4_ISR 23
#define BLINK_PERIOD 250

typedef unsigned char Byte_t;

Byte_t volatile Delay_counter;
bool volatile Led_state;

int
main() {
enableInterrupts();

/* LED output pin */
GPIOE->DDR |= (1 CR1 |= (1 ODR |= (1 PSCR = 0x05;

/* Auto-reload 124 */
TIM4->ARR = 0x7C;

/* Update interrupt */
TIM4->IER |= TIM4_IER_UIE;

/* Enable TIM 4 */
TIM4->CR1 |= TIM4_CR1_CEN;

while (true);

return 0;
}

void
Timer4_isr() __interrupt(TIM4_ISR) {
/* Reset update interrupt bit. */
TIM4->SR1 &= ~TIM4_SR1_UIF;

++Delay_counter;
if (Delay_counter > BLINK_PERIOD) {
Led_state = !Led_state;
Delay_counter = 0;
}

/* LED output control */
if (Led_state) {
GPIOE->ODR ^= (1 ODR |= (1

Attached: stm8s-8bit-microcontrollers-6-728.jpg (728x546, 71K)

Sweet fucking, what is wrong? How does your language not have static integer differentiation?

Haskell is not a functional programming language.

there is nothing wrong with that variable declaration besides 5 and .5 not being their own vars.

Why would you need THREE representations of ARITHMETIC RESULTANTS, IN ANY COMPUTATION?!

2.5, 0.5, 5 = Half

they are just morons or trolling

1.0 and 1f are the c double precision literals

>work on project
>try out critical library
>": Data.ByteString.hGetLine: end of file"
Oh... I-I guess I'll find another project to work on ;_;

listen man, i wasn't questioning his dumb question. Merely giving him an answer to it.

Ah, wasn't quite sure what gear to operate in.

Because the value of the things to divide depends on use input

wolframalpha.com/input/?i=((2.5/5 + 0.5/5) * (5/2.5 + 0.5/2.5) * (2.5/0.5 + 5/0.5))^(xyz+1)

Since when?

github.com/jhickner/smtp-mail/issues/21
Sigh...

wolframalpha.com/input/?i=(((2.5/5 + 0.5/5) * (5/2.5 + 0.5/2.5) * (2.5/0.5 + 5/0.5))^(xyz+1))/(c + \epsilon)^-x

can you draw benis with wolfram?

wolframalpha.com/input/?i=random phylum

I started reading "Prolog Programming for Artificial Intelligence", so far it seems really interesting and I can't wait to get to more practical parts of the language.

wolframalpha.com/input/?i=\delta^\pi^\phi^-3 = 4

Just to give some clarity to the definition I Want All Brothers Of Memory To Find One Day.

sup family
c++ dev reporting in
trying to raise my market value learning scripting shit

what are some must have juicy skills/libraries/frameworks/toolkits to dabble with? I use a lil bit of python, perl, js, sh, ps at work, still I spend 95% of my time with seeplusplus tho

grug wants to earn berries
what star-reading language should grug learn?

Write This Library, ASAP: wolframalpha.com/input/?i=1 + \iota = \psi/\epsilon = delta^(pi^phi^-2)

God Will Gift You All The Pussy Or Orifice Of Your Choosing.

Grug Berry-Belly-Full Picker Teacher

>still no gruglang

On my program it is determinate by the user
Just look at it pastebin.com/GV4TbdkH

black bean energy givers
or good sight orbs
or sight orbs for big brained grugs

on a scale from 0 to haskell, how useless do you plan it to be?

ok I'll come out clean since I didn't understand your answers
so I'm learning java and all this discussion between oopers and fpers is making me doubt about how much work will I get as freelance or whatever
is java actually a good language for starters? cuz oop is kinda boring so far. I've heard java is not a good language for beginners, but I just want to make quick bucks and I dunno if any beginner-friendly languages have high demand on the work market
what should I do?

They're calle programming challenges/problems for a reaosn. If you can do it, albeit slowly, then you have nothing to worry.
Some people are just really good at that type of problem-solving, other train really hard in order to get fast. in the end it, this user is right.

there are enough lisp dialects out there already.

If a bug lands on my monitor, instead of squishing it and ruining my monitor, I capture it with a layer of tape and throw it out.
It's still alive, it's just stuck on the tape.
I always wonder if in this state, the bugs will eventually reach a heightened sense of awareness, enlightenment, and peace with their demise. They may not be capable of that, but I consider it anyway.

I feel sorry for them, but I can't program with moths and "eye gnats" flying around the screen. You know?

>all this discussion between oopers and fpers is making me doubt about how much work will I get as freelance or whatever
anything you see on Jow Forums does not reflect the real world of programming

don't take those discussions seriously, java is still the de facto enterprise language
but it's also one of the easiest languages to outsource to third worlders

kotlin is a better java but most companies won't migrate their code, i mean most companies are still using java 8 / 9

you may find oop boring but that's kind of the point, it's supposed to reduce the complexity of large systems. but the problem is that most people don't do oop right. you know how c++ has a reputation for being unsafe, even if good programmers can write perfectly safe code? well that's because anyone can code in c++ which leads to a lot of idiots giving c++ a bad rap. this also happens for oop, anybody can make a class in java, but they do it wrong leading to some very ugly spaghetti code and now oop has a reputation for being bad. this also happens in fp, because most users are researches it has a reputation for not being practical

the fact is, those are all memes
java is useful. oop is good. fp is good.

dont act like the reputation of the language has nothing to do with the language itself

>anybody can code in c++
>anybody can code in javascript
rofl

Every time you fix a bug, your preventing your program from evolving.

Only feathered bipeds can code in JS.

>you may find oop boring but that's kind of the point, it's supposed to reduce the complexity of large systems
it doesn't do that as well as fp, though. oops is objectively inferior to fp

anybody with a cute pair of programming socks*

socks don't work unless you wear the whole outfit

for most use-cases, engineering panties + socks are all you need to produce flawless quality kode.

kys

no wonder devs these days are so dire. they don't wear the outfit

not him but how is fp superior? Literally nothing good is ever produced with them. even their tooling makes one consider C++ build systems a bliss.

there are some great things about expressive types when it comes to program safety

picture this
type order_type =
| Acknowledged
| Removed
| Filled of int * sign

let update_position order_type consolidated_position =
let change =
match order_type with
| Filled (size, sign) -> sign * size
| Acknowledged | Removed -> 0
in
consolidated_position + change

Now let's say you've got a new type of order

type order_type =
| Acknowledged
| Removed
| Filled of int * sign
| Busted of int * sign

The compiler will complain about the update_position function because you didn't pattern match against all cases. This is extremely useful in a system where safety is a priority. It removes a whole class of bugs.

A lot of great things are being produced with FP languages. They are, unfortunately, more difficult to grasp. So the run of the mill programmer will struggle too much with them for companies to widely adopt these languages.

>int * sign

it could be
>Filled of int * order_direction
And then have a function
type order_direction = Long | Short

let sign = function
| Long -> 1
| Short -> 1

And in your update position function
| Filled (size, order_direction) -> sign order_direction * size

An expressive type system blows any other type system out of the water.

> | Short -> -1
fixed

But again, this is the problem of FP. An average not-so-smart programmer has a lot of trouble with it.

>grug's face when seeing a complex type system

Attached: grug.png (235x215, 5K)

>it could be

>even their tooling makes one consider C++ build systems a bliss.

Attached: 1509830514594.png (745x720, 829K)

i don't think you understood how the expressive type worked and why it removed that entire category of bugs
understandable, i would say no more than 10% of programmers are able to reason about types

Simulation languages have that stuff, I think. Obviously you can just do two-dimensional arrays/vectors in C/C++, but would you really expect a technician to program properly?

why didn't you add an extra three sign fields huh? so you can negate the negation of the negation

Anything which looks easy to do is either already filled up or requires a lot of background knowledge and accurate, or decent, judgement.

t. Electrical Engineer into programming

I've known companies that didn't like hiring Comp Sci's because the compsci's were not-surprisingly, more theoretically focused and had trouble fitting into imperfect environments or projects where they had very little control.

So not only you didn't understand the importance of the type system. You also don't understand why having a DSL is good.

If you don't get why
>Fill (1500, Short)
is better than
>Fill (-1500)
You're beyond redemption

unsinged types were a mistake

Fill(-1500, Short)

>understandable, i would say no more than 10% of programmers are able to reason about types

>come work for us! we use shit tools and shit languages and no you can't write anything intelligent here
>what do you mean you want 300k or you're not interested?

you really don't get it at all don't you?

>no more than 10% of programmers are able to reason about types