[Haskell-cafe] Monad.Reader 8: Haskell, the new C++

[Manuel M T Chakravarty]

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.