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:
http://hpaste.org/2689
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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
