?

Log in

No account? Create an account
Функции на типах - Язык программирования Scala

> Recent Entries
> Archive
> Friends
> Profile
> Официальный сайт Scala

November 11th, 2013


Previous Entry Share Next Entry
dima_starosud
07:44 pm - Функции на типах
Здравствуйте товарищи!

Есть ли на Скала возможность построить "функцию", которая принимает тип и возвращает тип, как type family на Haskell?
Относится к этому вопросу, но я его хочу расширить, хочу теперь абстрагироваться от конкретных типов Int и Bool.

На Хаскеле выглядит так:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}

data ExprTag = BoolTag | NumTag

data Expr (tag :: ExprTag) where
    NumValue :: Expr NumTag
    BoolValue :: Expr BoolTag
    If :: Expr BoolTag -> Expr NumTag -> Expr NumTag -> Expr NumTag
    Add :: Expr NumTag -> Expr NumTag -> Expr NumTag

type family ExprType (tag :: ExprTag) (num :: *) (bool :: *) :: *
type instance ExprType BoolTag num bool = bool
type instance ExprType NumTag num bool = num

type Api num bool = (num, bool, num -> num -> num, bool -> num -> num -> num)

eval :: Api num bool -> Expr tag -> ExprType tag num bool
eval (num
     ,bool
     ,add :: num -> num -> num
     ,if_ :: bool -> num -> num -> num) = helper
    where
      helper :: Expr t -> ExprType t num bool
      helper NumValue = num
      helper BoolValue = bool
      helper (If b t e) = if_ (helper b) (helper t) (helper e)
      helper (Add n m) = helper n `add` helper m


Подскажите, пожалуйста, как это (ExprType tag num bool) сделать на Скала?
Большое спасибо :)

UPDATE: Снизошло такое решение, прошу критиковать.

trait ExprApi[B, N] {
  def num(): N
  def bool(): B
  def ifexpr(b: B, x: N, y: N): N
  def plus(x: N, y: N): N
}

trait Type {
  type Bool[B, N] = B
  type Num[B, N] = N
}

trait Expr[Type[_, _]] {
  def eval[B, N](api: ExprApi[B, N]): Type[B, N]
}

case class BoolValue extends Expr[Type#Bool] {
  def eval[B, N](api: ExprApi[B, N]): B = api.bool()
}

case class NumValue extends Expr[Type#Num] {
  def eval[B, N](api: ExprApi[B, N]): N = api.num()
}

case class IfExpr(
  b: Expr[Type#Bool],
  x: Expr[Type#Num],
  y: Expr[Type#Num]) extends Expr[Type#Num] {
  def eval[B, N](api: ExprApi[B, N]): N =
    api.ifexpr(b eval api, x eval api, y eval api)
}

case class Plus(
  x: Expr[Type#Num],
  y: Expr[Type#Num]) extends Expr[Type#Num] {
  def eval[B, N](api: ExprApi[B, N]): N =
    api.plus(x eval api, y eval api)
}

(12 comments | Leave a comment)

Comments:


[User Picture]
From:lomeo
Date:November 11th, 2013 07:47 pm (UTC)
(Link)
Я думаю, что это задача для type members.
From:dima_starosud
Date:November 11th, 2013 08:05 pm (UTC)
(Link)
Вы имеете ввиду типы спрятанные в классе?
С определенного ракурса весьма похоже на C++ный typedef - должно помочь.
[User Picture]
From:lomeo
Date:November 11th, 2013 08:33 pm (UTC)
(Link)
Да, я имел в виду path-dependent types.
Что-то вроде
trait Expr[T] { type Tag }
case class ENum(value: Int) extends Expr[Int] { type Tag = Int }
…
case class EIf[T](cond: Boolean, thenBranch: Expr[T], elseBranch: Expr[T]) extends Expr[T] { type Tag = T }
и
def eval[T](expr: Expr[T]): expr.Tag // если такое возможно

Я бы копал в эту сторону, но сходу не подскажу. Завтра подумаю.

Edited at 2013-11-11 08:33 pm (UTC)
[User Picture]
From:udpn
Date:November 15th, 2013 08:14 pm (UTC)
(Link)
Охренеть, у Expr же тип зависимый!11

(пошёл ботать Хаскелл дальше)
From:dima_starosud
Date:November 16th, 2013 07:02 pm (UTC)
(Link)
Вообще-то зависимые типы - это как монады: вы их используете всегда, даже не подозревая об этом.
И не только в Хаскеле, и не только в ФП.
eval, например, можно переписать в таком виде (и зависимых типов уже не видно):
evalBool :: Api num bool -> Expr BoolTag -> bool
evalBool api@(num, bool, add, if_) = helper
    where
      helper BoolValue = bool

evalNum :: Api num bool -> Expr NumTag -> num
evalNum api@(num, bool, add, if_) = helper
    where
      helper NumValue = num
      helper (If b t e) = if_ (evalBool api b) (helper t) (helper e)
      helper (Add n m) = helper n `add` helper m
From:Valentin Budaev
Date:November 17th, 2013 03:31 am (UTC)
(Link)
> вы их используете всегда, даже не подозревая об этом.

Ага, если вспомнить еще, что любой функциональный тип является частным случаем П-типа :)
[User Picture]
From:udpn
Date:November 17th, 2013 03:21 pm (UTC)
(Link)
Спасибо за справку, даже не знал, что такое зависимый тип, просто в голову почему-то пришло это странное сочетание двух слов.
From:Valentin Budaev
Date:November 17th, 2013 03:31 am (UTC)
(Link)
Не, просто с DataKinds хаскель автоматически лифтит значения в типы, а типы - в кайнды (где это можно), То есть это просто синтаксический сахар для type operators. Вот если бы можно было сделать инстанс семейства с аргументом лямбды - тип был бы зависимым.
[User Picture]
From:udpn
Date:November 17th, 2013 03:11 pm (UTC)
(Link)
Да понятно, что полноценные зависимые типы это не по адресу, но весьма таки неплохой сабсет. Теперь можно попробовать перевести вот это непотребство c C++ на Haskell. Не знал, что так можно.
From:Valentin Budaev
Date:November 17th, 2013 03:23 pm (UTC)
(Link)
Это не сабсет зависимых типов, это та вершина лямбда-куба, которая омега (только с несколько усложненной системой кайндов, но зато немного неполноценная с другой стороны, т.к. я как понимаю type family не может быть аргументом другой type family, поправьте, если ошибаюсь). А зависимые типы - совершенно другая вершина. Почему-то все вечно путают, константный терм в позиции типового аргумента смущает, видимо.
[User Picture]
From:udpn
Date:November 17th, 2013 04:51 pm (UTC)
(Link)
Expr зависит от значения типа ExprTag, и этот же ExprTag является типом, и такая штука вполне напоминает зависимые типы. ExprTag при этом и тип, и кайнд (напоминает мне cumulative universes или как их там называют). С другой стороны, у нас по-прежнему три уровня (значения-типы-кайнды), и это напоминает ту самую систем ф омега. На самом деле, это ни то, ни другое, каждый увидел в меру свой извращённости.
From:Valentin Budaev
Date:November 18th, 2013 12:52 pm (UTC)
(Link)
> Expr зависит от значения типа ExprTag, и этот же ExprTag является типом, и такая штука вполне напоминает зависимые типы.

Ну да, она _визуально_ напоминает, но выразительно - это совершенно не то :)

> Go to Top
LiveJournal.com