Tip azaltma sonsuz döngü

Question

Amacım bu gibi terimlerden () ortadan kaldırmaktır:

(a, b)  -> (a, b) 
((), b)  -> b 
(a, ((), b)) -> (a, b) 
... 

Ve bu kod şudur: bunu deneyerek, Ancak

{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE UndecidableInstances #-} 

module Simplify where 

import Data.Type.Bool 
import Data.Type.Equality 

type family Simplify x where 
    Simplify (op() x) = Simplify x 
    Simplify (op x()) = Simplify x 
    Simplify (op x y) = If (x == Simplify x && y == Simplify y) 
          (op x y) 
          (Simplify (op (Simplify x) (Simplify y))) 
    Simplify x   = x 

:

:kind! Simplify (String, Int) 

... tip denetleyicide sonsuz bir döngüye yol açar. Ben If tipi ailenin indirgenemez terimlerle ilgilenmesi gerektiğini düşünüyorum, ama açıkçası bir şey eksik. Ama ne?

Answer 1

Tip ailesi değerlendirmesi tembel değildir, bu yüzden If c t f tüm c, t ve f öğelerini değerlendirir. (Aslında, aile değerlendirme sırası şu anda gerçekten tanımlanmamıştır.) Sonsuz bir döngü ile sona erdirmek hiç de şaşırtıcı değil - Simplify (op x y) olsa bile, her zaman Simplify (op (Simplify x) (Simplify y))'u değerlendirin!

Çok gibi ayrı Rekursif basitleştirilmesi bölerek bu önleyebilirsiniz:

{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE UndecidableInstances #-} 

module Simplify where 

import Data.Type.Bool 
import Data.Type.Equality 

type family Simplify1 x where 
    Simplify1 (op() x) = x 
    Simplify1 (op x()) = x 
    Simplify1 (op x y) = op (Simplify1 x) (Simplify1 y) 
    Simplify1 x   = x 

type family SimplifyFix x x' where 
    SimplifyFix x x = x 
    SimplifyFix x x' = SimplifyFix x' (Simplify1 x') 

type Simplify x = SimplifyFix x (Simplify1 x) 

fikirdir:

1. Simplify1 basitleştirme bir adım yok.
2. SimplifyFix eşitse kontrol eder x ve tek aşamalı bir basitleştirme x' alır ve bunlar değilse (böylece Simplify1 sabit nokta bulma) basitleştirme bir adım yok.
3. SimplifySimplify1 numaralı çağrıyla SimplifyFix zincirinden çıkar. eşleşen tipi ailesi desen tembel olduğundan

, SimplifyFix doğru sonsuz döngüler önlenmesi, değerlendirme geciktirir.

Ve gerçekten:

*Simplify> :kind! Simplify (String, Int) 
Simplify (String, Int) :: * 
= (String, Int) 

*Simplify> :kind! Simplify (String, ((), (Int,()))) 
Simplify (String, ((), (Int,()))) :: * 
= ([Char], Int) 

Answer 2

Bir fixpoint karıştığı bu karmaşık çözümü oluşturmak için gerek yoktur, bunu sadeleştirme bir kat yapısına sahip olduğu göz önüne alındığında belirtmekte fayda var ifadesini yeniden erişir tekrar ve tekrar.

Bu sadece yeterli olacaktır: Bu size o tip düzeyinde hesaplama tembel varsayıyoruz görünüyor

{-# LANGUAGE TypeFamilies   #-} 
{-# LANGUAGE UndecidableInstances #-} 
module Simplify where 

type family Simplify x where 
    Simplify (op a b) = Op op (Simplify a) (Simplify b) 
    Simplify x  = x 

type family Op op a b where 
    Op op() b = b 
    Op op a() = a 
    Op op a b = op a b