DUBS TYPE PROPOSAL

This proposal aims to extend available numeric types in programming languages by adding the a dubs type. Objects of the type shall hold numeric values that terminate with repeating digits.

// Example usage in a C family language
dubs a = 11 // OK: 11 are sweet dubs
dubs b = 23 // error: 23 aren't sweet dubs

int c = 43 // OK: 43 is an int
dubs d = a // error: 43 aren't sweet dubs

fun f(dubs x) => x

f(100); // OK: 100 are dubs
f(101); // error: not dubs bro

fun g(int x) {
dubs y = x; // error: Not cool man. Can't fake dubs.
return x;
}

Base 10 only?

C doesn't have types, what passes for types is pointer size and access semantics(a float/int are both 4byte long and can be addressed/referenced within same line).#include <stdio.h>
int main(){

int a=392932244;
printf("%g",*((float*)&a));
}
C 'ints'/'floats'/strings are actually interface to pointers and machine instructions operating on them. Types are leaking abstraction that rears its "impelementation-specific" head every time there is an exploit or bug.
C++/Rust however do have genuine data types, and there is a trivial constructor/destructor mechanism to implement a dubs object or any type of numeric kind.

I had a dream about two females rubbing their sex organs together, is this 『ｄｕｂｓ』？？

>>4
If they were identical twin sisters it's dups tribbing, just as your state when posting that was dubs tripping.

>>1
Solution: use dependent types
open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)

data ℕ : Set where
succ : ℕ → ℕ
zero : ℕ

{-# BUILTIN NATURAL ℕ #-}

data vect {ℓ : Level} (A : Set ℓ) : ℕ → Set ℓ where
[] : vect A zero
_∷_ : {n : ℕ} → A → vect A n → vect A (succ n)
infixr 5 _∷_
infixr 4 _,_

data Σ {ℓ : Level} {ℓ′ : Level} {A : Set ℓ} (P : A → Set ℓ′) : Set (ℓ ⊔ ℓ′) where
_,_ : (a : A) → P a → Σ P

data ⊥ : Set where

data _≡_ {ℓ : Level} {A : Set ℓ} (x : A) : A → Set ℓ where
refl : x ≡ x

last2 : {ℓ : Level} → {A : Set ℓ} → {n : ℕ} → vect A (succ (succ n)) → vect A (succ (succ zero))
last2 (x ∷ (y ∷ [])) = x ∷ (y ∷ [])
last2 (_ ∷ (x ∷ (y ∷ xs))) = last2 (x ∷ (y ∷ xs))

car : {ℓ : Level} → {n : ℕ} → {A : Set ℓ} → vect A (succ n) → A
car (x ∷ _) = x

cdr : {ℓ : Level} → {n : ℕ} → {A : Set ℓ} → vect A (succ n) → vect A n
cdr (_ ∷ xs) = xs

dubs : ℕ → Set
dubs n = Σ (f n)
where f : (n : ℕ) → vect ℕ n → Set
f (succ (succ n)) x = let x' = last2 x in
car x' ≡ car (cdr x')
f _ _ = ⊥

--test : dubs 5
--test = (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [] , {!!}) -- goal: 3 ≡ 4, we can't do that!

test : dubs 5
test = (0 ∷ 1 ∷ 2 ∷ 3 ∷ 3 ∷ [] , refl)

-- works with bigger bases too! hex example:
test' : dubs 5
test' = (0 ∷ 1 ∷ 2 ∷ 15 ∷ 15 ∷ [] , refl)

Updated
open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsucc)

data ℕ : Set where
succ : ℕ → ℕ
zero : ℕ

{-# BUILTIN NATURAL ℕ #-}

data vect {ℓ : Level} (A : Set ℓ) : ℕ → Set ℓ where
[] : vect A zero
_∷_ : {n : ℕ} → A → vect A n → vect A (succ n)
infixr 5 _∷_
infixr 4 _,_

data Σ {ℓ : Level} {ℓ′ : Level} {A : Set ℓ} (P : A → Set ℓ′) : Set (ℓ ⊔ ℓ′) where
_,_ : (a : A) → P a → Σ P

data ⊥ {ℓ : Level} : Set ℓ where
data ⊤ : Set where
tt : ⊤

data _≡_ {ℓ : Level} {A : Set ℓ} (x : A) : A → Set ℓ where
refl : x ≡ x

last2 : {ℓ : Level} → {A : Set ℓ} → {n : ℕ} → vect A (succ (succ n)) → vect A (succ (succ zero))
last2 (x ∷ (y ∷ [])) = x ∷ (y ∷ [])
last2 (_ ∷ (x ∷ (y ∷ xs))) = last2 (x ∷ (y ∷ xs))

car : {ℓ : Level} → {n : ℕ} → {A : Set ℓ} → vect A (succ n) → A
car (x ∷ _) = x

cdr : {ℓ : Level} → {n : ℕ} → {A : Set ℓ} → vect A (succ n) → vect A n
cdr (_ ∷ xs) = xs

dubs : {ℓ : Level} → (Set ℓ) → ℕ → Set ℓ
dubs {ℓ} A n = Σ (f n)
where f : (n : ℕ) → vect A n → Set ℓ
f (succ (succ n)) x = let x' = last2 x in
car x' ≡ car (cdr x')
f _ _ = ⊥

--test : dubs 5
--test = (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [] , {!!}) -- goal: 3 ≡ 4, we can't do that!

test : dubs ℕ 5
test = (0 ∷ 1 ∷ 2 ∷ 3 ∷ 3 ∷ [] , refl)

-- works with bigger bases too! hex example:
test′ : dubs ℕ 5
test′ = (0 ∷ 1 ∷ 2 ∷ 15 ∷ 15 ∷ [] , refl)

-- non-number example:
test′′ : dubs Set 3
test′′ = (⊤ ∷ ⊥ ∷ ⊥ ∷ [] , refl)

Please rate

>>8
What programming language is this? It looks like Idris to me.

INTERCAL has a ``please'' keyword, so it must be INTERCAL.

>>9
Agda

>>10
I prefer interracial

https://i.4pcdn.org/pol/1589228378918.webm