the-type

A crate providing function which helps specifying type within the expression.

Motivation

Haskell allows type annotation for expression:

snoc (xs::[a])(x::a) = xs++[x] :: [a]

For Idris, the same function can be achieved by 'the' function

the : (ty : Type) -> ty -> ty
the ty x = x

There're also a RFC¹ and ongoing implementation² similar to the forementioned in Rust. This crate provide the function in library.

Usage

use the_type::the;
let foo: u8 = 0;

// typical method
let items1 : [usize; 4] = [foo.into(); 4];

// won't compile becuase Into is a generic trait but self.into() is not a generic method
// let items2 = [foo.into::<usize>(); 4];

// currently an experimental feature:
// let items3 = [foo.into(): usize; 4];

// an alternative way: 
let items4 = [usize::from(foo); 4];

// a more intuitive way:
let items5 = [the::<usize>(foo.into()); 4];