Как заставить типы из разных уровней типов в Haskell? - PullRequest
Новая
       69

Как заставить типы из разных уровней типов в Haskell?

2 голосов
/ 05 марта 2020

У меня есть следующий код: 

type Name = String

data Level = T0 | T1 | T2

data T (l :: Level) where
    Tint  :: T t
    Tdyn  :: T t
    Tbool :: T t
    Tarr  :: T 'T0 -> T 'T0 -> T t
    Tand  :: T 'T1 -> T 'T1 -> T 'T1
    Tarr2 :: T 'T1 -> T 'T2 -> T 'T2


class Arr (l1 :: Level) (l2 :: Level) (l3 :: Level) | l3 -> l1 l2 where
    infixr 3 ~>
    (~>) :: T l1 -> T l2 -> T l3

instance Arr 'T0 'T0 'T0 where 
    (~>) = Tarr 

instance Arr 'T0 'T0 'T1 where 
    (~>) = Tarr 

instance Arr 'T1 'T2 'T2 where
    (~>) = Tarr2

infixr 5 /\
(/\) :: T 'T1 -> T 'T1 -> T 'T1
(/\) = Tand

infixr 3 ~.>
(~.>) :: T 'T0 -> T 'T0 -> T t
(~.>) = Tarr

infixr 3 ~!>
(~!>) :: T 'T1 -> T 'T2 -> T 'T2
(~!>) = Tarr2

type Typ2 = T 'T2
type Typ1 = T 'T1
type Typ0 = T 'T0

int :: T t 
int = Tint

bool :: T t 
bool = Tbool

dyn :: T t
dyn = Tdyn

newType :: Typ2
newType = int /\ int ~> int /\ int ~> dyn



data Expr = Vi Int
          | Vb Bool
          | Vv Name
          | App Expr Expr
          | Lam Name Typ1 Expr
          deriving(Generic)

type Env = [(Name,Typ1)]

По сути, у меня есть три вида типов. T0, T1 и T2. Обратите внимание, что T0 также является T1, а T0 также является T2.

Я хотел бы написать проверку типа, хотя со следующей подписью: 

typecheck :: Expr -> Env -> [Typ2]

Требуется вызвать функцию с такой подписью: 

Name -> Env ->  [Typ0]

Проблема в том, что я не могу вернуть [Typ0] как [Typ2] в соответствии с компилятором, поэтому я предполагаю, что мне нужно выполнить приведение?

Кто-нибудь знает, что лучше всего делать в этой ситуации?

Редактировать: 

typecheck :: Expr -> Env -> [Typ2]
typecheck (Vv x) env = (envlookup x env)


envlookup :: Name -> Env ->  [Typ0]
envlookup name = 
    \case 
    (n,t):xs
        | n == name -> 
        case t of 
            int -> [int]
            -- otherwise -> t 
    [] -> []

1 Ответ

2 голосов
/ 05 марта 2020

Один из вариантов - написать функцию, которая повышает уровень типа: 

raise0 :: T T0 -> T t
raise0 Tint = Tint
raise0 Tdyn = Tdyn
raise0 Tbool = Tbool
raise0 (Tarr i e) = Tarr i e

В частности, это можно использовать для типа Typ0 -> Typ2. Другой способ заключается в том, чтобы типы вашей среды принимали уровень в качестве аргумента: 

envlookup :: Name -> Env t -> [T t]
envlookup name env = [t | (n, t) <- env, n == name]

Третий вариант - обеспечение возможности использования типов в средах на любом уровне: 

newtype AnyT = AnyT (forall t. T t)
type Env = [(Name, AnyT)]

envlookup :: Name -> Env -> [T t]
envlookup name env = [t | (n, AnyT t) <- env, n == name]
...