Francisco TolmaskyCan anyone familiar with Idris (or a different language with dependent types) confirm that types can *not* be used as values. For example, I can't make a list of types (a List that contains Int, Bool, and String directly). I also can't make a record that stores a type and an instance of that type (Like record TypeInstancePair { a :: Type, b :: a }). If so, is there a language that *does* allow this, and what is this feature called (other than "first-class types" which seems overloaded).
GNU social JP is a social network, courtesy of GNU social JP管理人. It runs on GNU social, version 2.0.2-dev, available under the GNU Affero General Public License.
All GNU social JP content and data are available under the Creative Commons Attribution 3.0 license.