In mathematics, an injective function or injection or one-to-one function is a function that preserves distinctness: it never maps distinct elements of its domain to the same element of its codomain. In other words, every element of the function's codomain is the image of at most one element of its domain. The term one-to-one function must not be confused with one-to-one correspondence (a.k.a. bijective function), which uniquely maps all elements in both domain and codomain to each other
Questions tagged [injective-function]
15 questions
13
votes
1 answer
Why can't we define closed data families?
All of the following work:
{-# LANGUAGE TypeFamilies #-}
type family TF a
type instance TF Int = String
type instance TF Bool = Char
data family DF a
data instance DF Int = DFInt String
data instance DF Bool = DFBool Char
type family CTF a where
…
leftaroundabout
- 117,950
- 5
- 174
- 319
5
votes
2 answers
How do we know all Coq constructors are injective and disjoint?
According to this course, all constructors (for inductive types) are injective and disjoint:
...Similar principles apply to all inductively defined types: all
constructors are injective, and the values built from distinct
constructors are never…
thor
- 21,418
- 31
- 87
- 173
3
votes
0 answers
How to prove that the type parameters of an Injective Type Family are Equivalent?
If I have an injective type family, and a proof of type equivalence, how can I get a proof of equivalence of the parameters?
The best I've been able to come up with uses unsafeCoerce, and it seems justified to me since the TypeFamily is injective,…
Josh.F
- 3,666
- 2
- 27
- 37
3
votes
1 answer
Automatic detection of domain for dependent type function in Idris
Idris language tutorial has simple and understandable example of the idea of Dependent Types:
http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#first-class-types
Here is the code:
isSingleton : Bool -> Type
isSingleton True =…
Shersh
- 9,019
- 3
- 33
- 61
2
votes
1 answer
Can I introduce sound constructor equivalence?
Say I've got an Inductive type like
Inductive foo :=
| a : foo
| b : foo
| c : foo.
but what I really want is to "identify" b with c - that is, I want to be able to treat them as two different ways of writing the same thing - and be able to…
Isaac van Bakel
- 1,772
- 10
- 22
2
votes
1 answer
Non-Injective Closed Type Family
I have this admittedly contrived chunk of code
{-# LANGUAGE DataKinds, TypeFamilies #-}
data Foo = Foo
type family Id (n :: Foo) a where
Id 'Foo a = a
data Bar (n :: Foo) = Bar
class Dispatch (n :: Foo) where
consume :: Id n a -> Bar n…
Silvio Mayolo
- 62,821
- 6
- 74
- 116
2
votes
1 answer
Type families and injectivity in a subset of indexes
I have the following type family:
{-# LANGUAGE TypeFamilyDependencies #-}
type family Const arr r = ret | ret -> r where
Const (_ -> a) r = Const a r
Const _ r = r
This is just the Const function in disguise, but the injectivity checker of…
Sebastian Graf
- 3,602
- 3
- 27
- 38
1
vote
1 answer
How to define observational equality in Agda
Let's say I have a render function:
rasterize : ℕ → ℕ → Tile → List (List Color
I need to prove this statement:
if rasterize w h t1 = rasterize w h t2 then t1 ≡ t2
in other words if t1 and t2 render to the same value given the same width and…
Farzad Bekran
- 489
- 1
- 6
- 13
0
votes
1 answer
Need Help Trying to Simplify this algorithm to map points on an arbitrarily large 2d plane to unique integers
So like the title says I need help trying to map points from a 2d plane to a number line in such a way that each point is associated with a unique positive integer. Put another way, I need a function f:ZxZ->Z+ and I need f to be injective.…
A-P
- 497
- 1
- 4
- 9
0
votes
1 answer
Generating Maximal Subsets of a Set Under Some Constraints in Python
I have a set of attributes A= {a1, a2, ...an} and a set of clusters C = {c1, c2, ... ck} and I have a set of correspondences COR which is a subset of A x C and |COR|<< A x C. Here is a sample set of correspondences
COR = {(a1, c1), (a1, c2), (a2,…
Muhammad Adeel Zahid
- 17,474
- 14
- 90
- 155
0
votes
0 answers
Examples of reduce functions that are injective?
Are there any sources to find common map-reduce functions that are injective ? (Is there a name for such functions ?)
For example, I need to map a list of numbers
lst = [1,2,3,4]
into a tuple (sum, product)
def mapper(lst):
sum_, prod = 0, 1
…
user12546101
0
votes
1 answer
How to help GHC infer that `Arrows (Domains func) (CoDomain func) ~ func`
Consider the Arrows, Domains and CoDomain type-families defined in the agda codebase.
Obvious to the programmer, it holds that Arrows (Domains func) (CoDomain func) ~ func. But I can't get curries (Proxy :: Proxy (Domains func)) (Proxy :: Proxy…
Sebastian Graf
- 3,602
- 3
- 27
- 38
0
votes
1 answer
Injective two-way mappings
I often deal with mappings which are injective. In programming terminology, this can be expressed as a dictionary where all values are unique as well as, of course, all keys.
Is there a memory-efficient data structure for injective mappings with all…
jpp
- 159,742
- 34
- 281
- 339
0
votes
1 answer
PK candidate must be an Injective, Surjective or Bijective function?
I have a doubt regarding information strength of a candidate to be a PK.
From my understanding, and this is what I want to share in order to check if it is correct, a PK candidate must be strong enough to uniquely identify a set of information,…
Daniel Ferreira Castro
- 324
- 3
- 22
-2
votes
1 answer
How to check if a hashmap is Injective (OneOnOne) in Java?
How do i write a method that can check if a hashmap is Injective (OneOnOne)? So that there is only one key for every value in the map. I want it so it can pass this test:
Map m = new HashMap();
…
Buffel
- 1
- 3