Tag Archives: types

Subtracting natural numbers: types and usability

Posted on February 7, 2023 by Brent

For several years now I have been working on a functional teaching language for discrete mathematics, called Disco. It has a strong static type system, subtyping, equirecursive algebraic types, built-in property-based testing, and mathematically-inspired syntax. If you want to know … Continue reading →

Posted in projects, teaching | Tagged , , , , | 3 Comments

Types for top-level definitions

Posted on August 27, 2022 by Brent

I’ve come up with idea for a type system for first-class (global) definitions, which can serve as a very lightweight alternative to a proper module system. I’m posting it here in the hopes of getting some feedback and pointers to … Continue reading →

Posted in projects | Tagged , , | 7 Comments

Implementing Hindley-Milner with the unification-fd library

Posted on September 8, 2021 by Brent

For a current project, I needed to implement type inference for a Hindley-Milner-based type system. (More about that project in an upcoming post!) If you don’t know, Hindley-Milner is what you get when you add polymorphism to the simply typed … Continue reading →

Posted in haskell, teaching | Tagged , , , | 3 Comments

Types versus sets in math and programming languages

Posted on June 24, 2021 by Brent

For several years I have been designing and implementing a functional teaching language especially for use in the context of a Discrete Mathematics course. The idea is for students to be exposed to some functional and statically-typed programming early in … Continue reading →

Posted in projects, teaching | Tagged , , , , , , | 10 Comments

Anafunctors

Posted on June 16, 2014 by Brent

This is part four in a series of posts on avoiding the axiom of choice (part one, part two, part three). In my previous post, we considered the “Axiom of Protoequivalence”—that is, the statement that every fully faithful, essentially surjective … Continue reading →

Posted in category theory, math, species | Tagged , , , , , , , , , , | 5 Comments

AC and equivalence of categories

Posted on June 5, 2014 by Brent

This is part three in a series of posts on avoiding the axiom of choice (part one, part two). In my previous post, I explained one place where the axiom of choice often shows up in category theory, namely, when … Continue reading →

Posted in category theory, math, species | Tagged , , , , , , , , , | 5 Comments

Unique isomorphism and generalized “the”

Posted on May 13, 2014 by Brent

This is part two in a series of posts on avoiding the axiom of choice; you can read part one here. In category theory, one is typically interested in specifying objects only up to unique isomorphism. In fact, definitions which … Continue reading →

Posted in category theory, math, species | Tagged , , , , , , , , | 8 Comments

Avoiding the axiom of choice, part I

Posted on May 8, 2014 by Brent

I’m hard at work on my dissertation, and plan to get back to doing a bit of blogging based on stuff I’m writing and thinking about, as a way of forcing myself to explain things clearly and to potentially get … Continue reading →

Posted in category theory, math, species | Tagged , , , , , | 17 Comments

Unordered tuples and type algebra

Posted on August 24, 2012 by Brent

At Hac Phi a few weekends ago (which, by the way, was awesome), Dan Doel told me about a certain curiosity in type algebra, and we ended up working out a bunch more details together with Gershom Bazerman, Scott Walck, … Continue reading →

Posted in combinatorics | Tagged , , , , | 7 Comments

Typed type-level programming: status report

Posted on December 3, 2010 by Brent

A few people have been bugging me (you know who you are ;-) about the current status of the project to allow automatic “lifting” of Haskell data constructors to the type level, to allow for typed type-level programming. I’ve written … Continue reading →

Posted in haskell, projects | Tagged , , , , , , | Leave a comment