[Agda] Friday afternoon magic

[Andreas Abel]

I can shut off Phantom types in no time, then the magic will 
disappear... ;-)

Confession: I did not solve the exercise, I cheated with Agda.

Andreas

On 22.03.13 1:35 PM, Nils Anders Danielsson wrote:
> Hi,
>
> Some readers of this list may enjoy the following exercise: explain why
> "works" type-checks, but "fails" doesn't.
>
> module Magic where
>
> data Bool : Set where
>    true false : Bool
>
> data Bool′ (A : Set) : Set where
>    true false : Bool′ A
>
> to : (A : Set) → Bool → Bool′ A
> to _ true  = true
> to _ false = false
>
> from : (A : Set) → Bool′ A → Bool
> from _ true  = true
> from _ false = false
>
> magic : (A : Set) → Bool → Bool
> magic A b = from A (to A b)
>
> f₁ : Bool → Bool → Bool
> f₁ false false = true
> f₁ _     _     = true
>
> f₂ : Bool → Bool → Bool
> f₂ b₁ b₂ = magic Empty (f₁ b₁ b₂)
>    where
>    data Empty : Set where
>
> data P (f : Bool → Bool → Bool) : (Bool → Bool) → Set where
>    p : (b : Bool) → P f (f b)
>
> fails : P f₁ (f₁ false)
> fails = p _  -- Unsolved constraint: (f₁ _24 x) = (f₁ false x) : Bool.
>
> works : P f₂ (f₂ false)
> works = p _  -- No unsolved constraints.
>

-- 
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/