[Haskell-cafe] Monad.Reader 8: Haskell, the new C++
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Thu Sep 13 21:25:09 EDT 2007
Derek Elkins wrote,
> On Thu, 2007-09-13 at 11:12 -0700, Don Stewart wrote:
>>>> Better here means "better" -- a functional language on the type
>>>> to type a functional language on the value level.
>>>> -- Don
>>> For a taste, see Instant Insanity transliterated in this functional
>>> NB: it took me 5 minutes, and that was my first piece of coding ever
>>> with Type families
>> Wow. Great work!
>> The new age of type hackery has dawned.
> Is the type level functional language non-strict? (Is there a flag that
> will allow non-terminating associated type programs?)
The associated type theory is only concerned with terminating (aka
strongly normalising) sets of type instances. For a strongly
normalising calculus, it does not matter whether you use eager or
However, there is of course a flag to diable the check for
termination and to give up on decidable type checking. It's the
same flag as for type classes: -fallow-undecidable-instances
(Equations of type families, or type-level functions, are introduced
with the keywords "type instance", so the option name still makes
FWIW, the evaluation strategy in this case is right now fairly
eager, but it is a little hard to characterise. If the application
of a type family needs to be normalised to proceed with unification, eg,
[a] ~ F (G Int)
then F (G Int) will be eagerly evaluated (ie, first G Int, and then
(F <result of G Int>). However, type-level data constructors (ie,
type constructors are non-strict); eg,
[a] ~ [F Int]
will result in the substitution [F Int/a]. And you can use cyclic
a ~ F a
However, they must have a finite solution, as we still only admit
finite types; eg, the following definition of F would be fine:
type family F a
type instance F a = Int
type family F a
type instance F a = [a]
will give you one of these "cannot construct infinite type: a ~ [a]"
messages. This makes it a bit like Id/pH's lenient evaluation.
 This is GHC after all, it tries to gently nudge you in the right
direction, but if you insist, it happily let's you drill
arbitrarily large holes in your foot.
More information about the Haskell-Cafe