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 system, to type a functional language on the value level.
-- Don For a taste, see Instant Insanity transliterated in this functional language:
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 non-strict evaluation. However, there is of course a flag to diable the check for termination and to give up on decidable type checking.[1] 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 sense.) 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 bindings: 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 but 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. Manuel [1] 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.