gradual typing [Re: [Agda] Compile-time parsing]

[Andreas Abel]

On 12/16/11 2:37 PM, Conor McBride wrote:
> Anywhere you have an A where you want a B, you can insert
> an explicit coercion by a metavariable proof that A equals B.
> The Epigram elaborator (such as it is) uses this approach to
> handle the "change of direction" rule in bidirectional
> checking. In that setting, there are no errors, only proof
> obligations which turn out to be a bit tricky.

What is missing is a proper treatment of this cast by the compiler(s), 
then we have gradual typing.  Roughly

postulate
   cast : forall {a}{A : Set a}{B : Set a}{eq : A == B} -> A -> B

{-# COMPILED cast unsafeCoerce #-}

For the "I know what I am doing (or at least I think so)" dependently 
typed programmer.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/