# Function that only accepts odd number argument

**URL:** https://discourse.julialang.org/t/function-that-only-accepts-odd-number-argument/27502
**Category:** General Usage
**Tags:** type
**Created:** [August 13, 2019, 4:12pm UTC](https://discourse.julialang.org/t/function-that-only-accepts-odd-number-argument/27502 "2019-08-13T16:12:41Z")
**Posts on this page:** 1
**Showing post:** 10

<div class="post-metadata">

### Author: ![chakravala](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/chakravala/32/6832_2.png) [@chakravala](https://discourse.julialang.org/u/chakravala)
#### Post date: [August 14, 2019, 12:48pm UTC](https://discourse.julialang.org/t/function-that-only-accepts-odd-number-argument/27502/10 "2019-08-14T12:48:17Z")

</div>

This is precisly the sort of thing you could do if we finally had implemented `inductive` types in Julia

> **[Inductive type](https://en.m.wikipedia.org/wiki/Inductive_type)**
>
> In type theory, a system has inductive types if it has facilities for creating a new type from constants and functions that create terms of that type. The feature serves a role similar to data structures in a programming language and allows a type theory to add concepts like numbers, relations, and trees. As the name suggests, inductive types can be self-referential, but usually only in a way that permits structural recursion.
> The standard example is encoding the natural numbers using Peano's ...

> [@Julia with respect to reliability, sustainability, critical application, dynamic/static typing, big data, HPC?](https://discourse.julialang.org/t/julia-with-respect-to-reliability-sustainability-critical-application-dynamic-static-typing-big-data-hpc/23135/14):
>
> Another formalistic language I want Julia to learn from is [agda](https://en.wikipedia.org/wiki/Agda_(programming_language)).
> 
> > Programming in pure type theory involves a lot of tedious and repetitive proofs, and Agda has no support for tactics. Instead, Agda has support for automation via [reflection](https://en.wikipedia.org/wiki/Reflection_(computer_programming)). The reflection mechanism allows one to quote program fragments into – or unquote them from – the abstract syntax tree. The way reflection is used is similar to the way Template Haskell works.[[8]](https://en.wikipedia.org/wiki/Agda_(programming_language)#cite_note-8)
> 
> Reflection is also what Julia metaprogramming is based on, so extend the type system of Julia?

> [@Julia with respect to reliability, sustainability, critical application, dynamic/static typing, big data, HPC?](https://discourse.julialang.org/t/julia-with-respect-to-reliability-sustainability-critical-application-dynamic-static-typing-big-data-hpc/23135/17):
>
> The new features don’t have to exactly resemble a previous language, just learn from it.
> 
> Are [inductive types](https://en.m.wikipedia.org/wiki/Inductive_type) threatening to other aspects of the Julia language that would cause trade-off?

> [@Julia with respect to reliability, sustainability, critical application, dynamic/static typing, big data, HPC?](https://discourse.julialang.org/t/julia-with-respect-to-reliability-sustainability-critical-application-dynamic-static-typing-big-data-hpc/23135/19):
>
> A new keyword like `inductive type` could be used to generalize Julia from only type dispatch to make julia able of more general proofs.

> [@Julia with respect to reliability, sustainability, critical application, dynamic/static typing, big data, HPC?](https://discourse.julialang.org/t/julia-with-respect-to-reliability-sustainability-critical-application-dynamic-static-typing-big-data-hpc/23135/21):
>
> The only reason I mention it is purely due to my interest in the mathematics of it, I recommend looking at the referenced paper [Engineering Proof by Reflection in Agda](http://hal.inria.fr/docs/00/98/76/10/PDF/ReflectionProofs.pdf)
> 
> > Abstract. This paper explores the recent addition to Agda enabling reflection, in the style of Lisp and Template Haskell. It gives a brief introduction to using reflection, and details the complexities encountered when automating certain proofs with proof by reflection. It presents a library that can be used for automatically quoting a class of concrete Agda terms to a non-dependent, user-defined inductive data type, alleviating some of the burden a programmer faces when using reflection in a practical setting.

What you want is an `inductive` type so that the type system can make formal proofs about odd and even integers… I’ve been wanting this for a long time now.

@jeff.bezanson this is on more people’s wishlist now!

---

_[View the full topic](https://discourse.julialang.org/t/function-that-only-accepts-odd-number-argument/27502)._