wyższego rzędu konstruktorów typu i funktory w SML

Question

można następujące funkcje polimorficzne

let id x = x;; 
let compose f g x = f (g x);; 
let rec fix f = f (fix f);;  (*laziness aside*) 

być napisane dla typów/konstruktorów typu lub modułów/funktorów? Próbowałem dla niektórych typów, ale nie działa.

Oto wersja Haskell dla typów:

data Id x = Id x 
data Compose f g x = Compose (f (g x)) 
data Fix f = Fix (f (Fix f)) 

-- examples: 
l = Compose [Just 'a'] :: Compose [] Maybe Char 

type Natural = Fix Maybe -- natural numbers are fixpoint of Maybe 
n = Fix (Just (Fix (Just (Fix Nothing)))) :: Natural -- n is 2 

-- up to isomorphism composition of identity and f is f: 
iso :: Compose Id f x -> f x 
iso (Compose (Id a)) = a 

Answer 1

Haskell pozwala wpisać zmienne wyższego rodzaju. Dialekty ML, w tym Caml, dopuszczają tylko zmienne typu "*". Tłumaczone na prostym języku angielskim,

• W Haskell, typ zmiennej g może odpowiadać „konstruktora typu” jak Maybe lub IO lub list. Tak więc g x w twoim przykładzie Haskell byłoby OK (żargon: "dobrze-dopieszczony"), jeśli na przykład g jest Maybe i x jest Integer.

• w ml, typ zmiennej 'g mogą odpowiadać jedynie do „rodzaju gruntu” jak int lub string, nigdy do konstruktora typu jak option lub list. Dlatego jest to prawidłowe, aby próbować zastosować zmienną typu do innego typu.

O ile mi wiadomo, nie ma głębokiej przyczyny tego ograniczenia w ML. Najbardziej prawdopodobnym wyjaśnieniem jest historyczny przypadek. Kiedy Milner początkowo wymyślił swoje koncepcje dotyczące polimorfizmu, pracował z bardzo prostymi zmiennymi typu stojącymi tylko za monotypami rodzaju *. Wczesne wersje Haskella robiły to samo, a potem Mark Jones odkrył, że wnioskowanie o rodzajach zmiennych jest całkiem proste. Haskell został szybko zmieniony, aby umożliwić zmienne typu wyższego rodzaju, ale ML nigdy go nie dogonił.

Ludzie z INRII wprowadzili wiele innych zmian w ML i jestem nieco zaskoczony, że nigdy tego nie zrobili. Kiedy programuję w ML, może mi się podobać posiadanie zmiennych o wyższych parametrach. Ale ich tam nie ma i nie znam żadnego sposobu na zakodowanie przykładów, o których mówisz, chyba że używasz functors.

Answer 2

Możesz zrobić coś podobnego w OCaml, używając modułów zamiast typów i funktorów (moduły wyższego rzędu) zamiast typów wyższego rzędu. Wygląda jednak o wiele brzydiej i nie ma zdolności do wnioskowania o typ, więc musisz ręcznie określić wiele rzeczy.

module type Type = sig 
    type t 
end 

module Char = struct 
    type t = char 
end 

module List (X:Type) = struct 
    type t = X.t list 
end 

module Maybe (X:Type) = struct 
    type t = X.t option 
end 

(* In the following, I decided to omit the redundant 
    single constructors "Id of ...", "Compose of ...", since 
    they don't help in OCaml since we can't use inference *) 

module Id (X:Type) = X 

module Compose 
    (F:functor(Z:Type)->Type) 
    (G:functor(Y:Type)->Type) 
    (X:Type) = F(G(X)) 

let l : Compose(List)(Maybe)(Char).t = [Some 'a'] 

module Example2 (F:functor(Y:Type)->Type) (X:Type) = struct 
    (* unlike types, "free" module variables are not allowed, 
    so we have to put it inside another functor in order 
    to scope F and X *) 
    let iso (a:Compose(Id)(F)(X).t) : F(X).t = a 
end 

Answer 3

Cóż ... Nie jestem ekspertem od typów wyższego rzędu ani programowaniem Haskella. Ale to wydaje się być ok dla F # (co jest OCaml), można pracować z nich:

type 'x id = Id of 'x;; 
type 'f fix = Fix of ('f fix -> 'f);; 
type ('f,'g,'x) compose = Compose of ('f ->'g -> 'x);; 

ostatni I zawinięte do krotki jak nie wymyślić nic lepszego ...

Answer 4

Można to zrobić, ale trzeba zrobić trochę trick:

newtype Fix f = In{out:: f (Fix f)} 

Można zdefiniować Cata potem:

Cata :: (Functor f) => (f a -> a) -> Fix f -> a 
Cata f = f.(fmap (cata f)).out 

To będzie określić ogólny catamorphism dla wszystkich funktorów, które możesz użyć do budowania własnych rzeczy. Przykład:

data ListFix a b = Nil | Cons a b 
data List a = Fix (ListFix a) 
instance functor (ListFix a) where 
fmap f Nil = Nil 
fmap f (Cons a lst) = Cons a (f lst)