Loại giảm vòng lặp vô hạn

Question

Mục tiêu của tôi là để loại bỏ () từ các thuật ngữ, như thế này:

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

Và đây là đoạn code:

{-# 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 

Tuy nhiên, cố gắng nó ra:

:kind! Simplify (String, Int) 

... dẫn đến vòng lặp vô hạn trong trình kiểm tra loại. Tôi nghĩ rằng gia đình loại If nên được chăm sóc của các điều khoản irreducible, nhưng tôi rõ ràng là thiếu một cái gì đó. Nhưng cái gì?

Answer 1

Nhập đánh giá gia đình không phải là lười biếng, vì vậy If c t f sẽ đánh giá tất cả c, t và f. (Thực tế, loại đánh giá gia đình không thực sự được xác định ngay bây giờ.) Vì vậy, không có gì lạ khi bạn kết thúc với một vòng lặp vô hạn - bạn luôn đánh giá Simplify (op (Simplify x) (Simplify y)), ngay cả khi đó là Simplify (op x y)!

Bạn có thể tránh điều này bằng cách phân chia các đệ quy và đơn giản hóa ngoài, như vậy:

{-# 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) 

Ý tưởng là:

1. Simplify1 làm một bước đơn giản hóa.
2. SimplifyFix mất x và đơn giản hóa một bước x', kiểm tra xem chúng có bằng nhau không và nếu chúng không thực hiện một bước đơn giản hóa khác (do đó tìm điểm cố định là Simplify1).
3. Simplify chỉ cần bắt đầu chuỗi SimplifyFix với cuộc gọi đến Simplify1.

Vì kiểu gia đình khớp mẫu là lười biếng, SimplifyFix đánh giá trễ chính xác, ngăn chặn vòng vô hạn.

Và quả thực:

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

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

Answer 2

tôi nghĩ rằng tôi muốn đề cập đến việc cho rằng đơn giản hóa có cấu trúc của một lần, không có nhu cầu để xây dựng giải pháp phức tạp này liên quan đến một fixpoint mà lại đi qua các biểu hiện lặp đi lặp lại.

này sẽ làm tốt:

{-# 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