this post was submitted on 05 Aug 2023
8 points (100.0% liked)

Programming Languages

1167 readers
7 users here now

Hello!

This is the current Lemmy equivalent of https://www.reddit.com/r/ProgrammingLanguages/.

The content and rules are the same here as they are over there. Taken directly from the /r/ProgrammingLanguages overview:

This community is dedicated to the theory, design and implementation of programming languages.

Be nice to each other. Flame wars and rants are not welcomed. Please also put some effort into your post.

This isn't the right place to ask questions such as "What language should I use for X", "what language should I learn", and "what's your favorite language". Such questions should be posted in /c/learn_programming or /c/programming.

This is the right place for posts like the following:

See /r/ProgrammingLanguages for specific examples

Related online communities

founded 1 year ago
MODERATORS
 

While working with a dynamically typed lang, I came across this:

hash(password, algorithm, algorithmOptions)

Where algorithm is a constant signaling which hashing algorithm to use, and algorithmOptions is a dict whose keys depend on algorithm.

So I thought, can we dictate that if a previous parameter has this value, then this parameter has to have this other value?

E.g.

enum HashAlgo {
    Bcrypt,
    Argon2,
}

type BcryptOptions = {
    Int optionA,
    Int optionB,
}

type Argon2Options = {
    String optionC,
    String optionD,
}


// Here I make this type "depend" on an argument of type HashAlgo
type HashOptions = [HashAlgo] => {
    HashAlgo::Bcrypt => BcryptOptions,
    HashAlgo::Argon2 => Argon2Options,
}

fun hash(
    String password,
    HashAlgo algorithm,
    // Here I use HashOptions, passing the prev. argument
    HashOptions[algorithm] options,
)

This way the compiler can ensure the correct dict is used, based on the value of algorithm

Does something like this exist? I now realize that it would be impossible to type check in compile time based on a runtime value, but if it was allowed only for constants? What do you think?

you are viewing a single comment's thread
view the rest of the comments
[–] armchair_progamer@programming.dev 5 points 1 year ago* (last edited 1 year ago)

Multiple ways you can do this. Most of these should also extend to multiple arguments, and although the constant is promoted to type level, you can pass it around nested functions as a type parameter.

With generics

In Java (personally I think this approach is best way to implement your specific example; also Kotlin, C#, and some others are similar):

interface HashAlgo<Options> {
    String hash(String password, Options options);
}

class Bcrypt implements HashAlgo<BcryptOptions> { ... }
class Argon2 implements HashAlgo<Argon2Options> { ... }
record BcryptOptions { ... }
record Argon2Options { ... }

In Haskell without GADTs (also Rust is similar):

class HashAlgo opts where
  hash :: String -> opts -> String

data BcryptOptions = BcryptOptions { ... }
data Argon2Options = Argon2Options { ... }

instance HashAlgo BcryptOptions where
  hash password BcryptOptions { .. } = ...

instance HashAlgo Argon2Options where
  hash password Argon2Options { .. } = ...

In C (with _Generic):

typedef struct { ... } bcrypt_options;
typedef struct { ... } argon2_options;

char* hash_bcrypt(const char* password, bcrypt_options options) { ... }
char* hash_argon2(const char* password, argon2_options options) { ... }

#define hash(password, options) _Generic((options), bcrypt_options: hash_bcrypt, argon2_options: hash_argon2)(password, options)

In TypeScript, inverting which type is parameterized (see this StackOverflow question for another TypeScript approach):

type HashAlgo = 'bcrypt' | 'argon2'
type HashOptions<H> = H extends 'bcrypt' ? BcryptOptions : H extends 'argon2' ? ArgonOptions : never

function hash<H>(password: string, algorithm: H, options: HashOptions<H>): string { ... }

With constant generics or full dependent types

This way is a bit more straightforward but also way more complicated for the compiler, and most languages don't have these features or they're very experimental. Dependent types are useful when your constant is non-trivial to compute and you can't even compute it fully, like vectors with their length as a type parameter and append guarantees the return vector's length is the sum. In that case generics aren't enough. Constant generics aren't full dependent types but let you do things like the vector-sum example.

In Haskell with GADTs AKA Generic Algebraic Data types (also works in Idris, Agda, and other Haskell-likes; you can simulate in Rust using GATs AKA Generic Associated Types, but it's much uglier):

data BcryptOptions = BcryptOptions { ... }
data Argon2Options = Argon2Options { ... }
data Algorithm opts where
    Bcrypt :: Algorithm BcryptOptions
    Argon2 :: Algorithm Argon2Options

hash :: String -> Algorithm opts -> opts -> String
hash password algo opts =
    case algo of
    | Bcrypt -> ... -- opts is inferred to be BcryptOptions here
    | Argon2 -> ... -- opts is inferred to be Argon2Options here

In Coq (also flipping the parameterized types again):

Inductive algorithm : Set := bcrypt | argon2.
Inductive algorithm_options (A: algorithm) : Set := bcrypt_options : ... -> algorithm_options bcrypt | argon2_options : ... -> algorithm_options argon2.

Fixpoint hash (password : string) (algo : algorithm) (opts : algorithm_options also) : string := ... .