Идрис 01

comments

-- single-line

{-
      multi-line
-}

keywords

      case .. of
      constructor
      data
      export
      if .. then .. else ..
      implementation
      import
      interface
      let .. in
      module
      mutual
      namespace
      parameters
      private
      public export
      record
      total
      using
      where

primitive types:

      Int
      Integer
      Double
      Char
      String
      Bool : True | False
      Ptr 
      Bits8
      Bits16
      Bits32
      Bits64

ops

      +             Int, Double, Bits8, Bits16, Bits32, Bits64
      -             Int, Double, Bits8, Bits16, Bits32, Bits64

      *             Int, Double

      /             Double

      ++            String

      div           Int
      divBigInt     Integer
      divInt        Int

      mod           Int
      modBigInt     Integer
      modInt        Int


      gcd           Int
      lcm           Int

      ||            Bool
      &&            Bool
      not           Bool

      /=            Eq t 
      ==            Eq t 

      <             Ord t
      <=            Ord t
      >             Ord t
      >=            Ord t

      max           Ord t
      min           Ord t

bits ops

     divB8
     divB16
     divB32
     divB64

     modB8
     modB16
     modB32
     modB64

type casting

  cast : Cast fm to => (orig : fm) -> to

  the : (a : Type) -> a -> a

  fromInteger : Num ty => Integer -> ty

  unpack : String -> List Char

     > unpack "ABC"
      ['A', 'B', 'C']

  pack : Foldable t => t Char -> String

     > pack ['A', 'B', 'C']
      "ABC" : String

  words : String -> List String

-- разделяет строку по пробелам

    > words " A B C  D E   "
      ["A", "B", "C", "D", "E"]

  unwords : List String -> String

-- склеивает строки, с пробелами-разделителями

    > unwords ["A", "BC", "D", "E"]
      "A BC D E"

  lines : String -> List String

-- разбивает строку по знаку "новой строки"

    > lines "\rA BC\nD\r\nE\n"
     ["A BC", "D", "E"]

  unlines : List String -> String

-- склеивает строки, с разделителями-"новая строка"

    > unlines ["line", "line2", "ln3", "D"]
     "line\nline2\nln3\nD"

  b8ToString  : Bits8  -> String
  b16ToString : Bits16 -> String
  b32ToString : Bits32 -> String
  b64ToString : Bits64 -> String

modules

файл модуля состоит из
- опциональной декларации module <name> за которой следуют
- опциональный список import <name>
- декларации и определения

программа может состоять из нескольких модулей и каждый из них имеет отдельное пространство имен. имя модуля не обязано совпадать с именем файла, хотя это приветствуется

в декларации import ссылаются на имя файла используя "dots separated directories":

   import foo.bar 

импортирует файл "foo/bar.idr", с его внутренней декларацией:

   module foo.bar

главный модуль программы должен содержать декларацию module Main и функцию main, а вот имя его не обязано быть Main.idr

функции, типы и интерфейсы могут быть помечены как private, export или public export. по умолчанию все имена модуля являются private

• private
• export       экспортируется только самый верхний уровень
• public export

для функций:

export       экспортируется тип

public export       экспортируется тип и определение

для типов данных:

export       экспортируется конструктор типа

public export       экспортируется конструктор типа и конструктор данных

для интерфейсов:

export       экспортируется имя

public export       экспортируется имя, методы и дефолтные определения

тип экспорта может быть изменен с помощью директивы %access :

    module Btree

    %access export

и теперь любая функция без директивы доступа будет иметь тип export, а не private

определив модуль вы определяете и пространство имен. пространства имен могут определяться и явно:

   module Foo

   namespace x
     test : Int -> Int
     test x = x * 2

   namespace y
     test : String -> String
     test x = x ++ x

functions

в отличие от Хаскеля в Идрисе и типы и функции могут начинаться как с заглавной, так и со строчной букв - имена функций, конструкторы (данных и типов) находятся в одном пространстве имен

where

локальную функцию можно определить используя where. все имена, видимые в самой функции видны и в блоке where. имя, которое определено в сигнатуре, но не в основном теле - будет видно в where если оно является параметром типа. функции, определенные в where требуют сигнатуры

let x = ... in ...

допускается паттерн-матчинг

case ... of ...

* в каждой ветке матчится один и тот же тип и возвращается один и тот же тип

* тип результата должен определяться тайпчекером без проверки тела case ... if

функция, вычисляющая тип

    f01 : Bool -> Type 
    f01 True = Nat 
    f01 False = List Nat    

может быть использована как return type

    f02 : (x : Bool) -> f01 x 
    f02 True = 0 
    f02 False = []    

так и в середине сигнатур

    f03 : (x : Bool) -> f01 x -> Nat 
    f03 True y = y 
    f03 False [] = 0 
    f03 False (y :: ys) = y + f03 False ys    

любое имя со строчной начальной, появляющееся как параметр или индекс в сигнатуре всегда будет неявным аргументом, который может быть задан и явно в теле функции с помощью {a = value}:

   f04 : Fin n -> Vect n a -> a 
   f04 FZ     (x :: xs) = x 
   f04 (FS k) (x :: xs) = g03 k xs

   f05 : Int 
   f05 = g04 {a=Int} {n=2} FZ (2 :: 3 :: Nil)    

ключевое слово using позволяет задать сигнатуры для всех НЕЯВНЫХ переменных и типов в декларациях и определениях блока:

   using (x : a, y : a, xs : Vect n a)

     data Elem : a -> Vect n a -> Type where
       Here  : Elem x (x :: xs) 
       There : Elem x xs -> Elem x (y :: xs)    

набор функций может быть параметризован аргументами, если используется ключевое слово parameters с перечнем аргументов перед декларацией этих функций:

   parameters (x : Nat, y : Nat)

     addAll : Nat -> Nat
     addAll z = x + y + z    

такие параметры передаются ПЕРЕД явными параметрами в каждой функции блока

ключевым словом mutual задается блок взаимно-рекурсивных функций

  
    mutual
      even : Nat -> Bool
      even Z = True
      even (S k) = odd k

      odd : Nat -> Bool
      odd Z = False
      odd (S k) = even k

в Идрисе есть хаскельные "секции":

  λΠ> :let z : Vect 5 Int ; z = [1, 2, 3, 4, 5] 
  λΠ> show $ map (* 2) z
  "[2, 4, 6, 8, 10]" : String      

используя ключевое слово total перед декларацией функции можно потребовать от компилятора проверки этой функции на тотальность

tuples

встроенный тип данных:

   data Pair : (a : Type) -> (b : Type) -> Type where
     MkPair : (a : A) -> (b : B) -> (A , B)     

синтаксический сахар (a , b) означает либо Pair a b либо MkPair a b - в зависимости от контекста

      λΠ> :let x = MkPair 10 "aaa"
       defined
      λΠ> x
      (10, "aaa") : (Integer, String)
      λΠ> fst x
      10 : Integer
      λΠ> snd x
      "aaa" : String
      λΠ> :let y = (True, x)
       defined
      λΠ> y
       (True, 10, "aaa") : (Bool, Int, String)
      λΠ> :let z = fst (snd y)
       defined
      λΠ> z
       10 : Int
  

records

синтакс отличен от Haskell:

    record Person where
      constructor MkPerson 
      firstName, middleName, lastName : String 
      age : Int
      member : Bool  

    fred : Person 
    fred = MkPerson "Fred" "Joe" "Bloggs" 30 True  

каждая запись определяет свое собственное пространство имен, так что имена полей разных записей могут совпадать

    jim : Person 
    jim = record { firstName = "Jim" } fred  

синтакс record { field = val, ... } var создает функцию, которая для существующей записи var обновляет указанные поля новыми значениями. поля могут быть зависимыми типами - в этом случае обновление произойдет только если результат имеет правильный тип

IO

    show     : Show a => a -> String
    print    : Show a => a -> IO ()
    printLn  : Show a => a -> IO ()
 
    putStr    : String -> IO ()
    putStrLn  : String -> IO ()
    putChar   : Char -> IO ()
    putCharLn : Char -> IO ()

    getLine  : IO String
    getChar  : IO Char
    getArgs  : IO (List String)


    data File : Type where
      FHandle : (p : Ptr) -> File

    data Mode : Type
      Read              : Mode
      WriteTruncate     : Mode
      Append            : Mode
      ReadWrite         : Mode
      ReadWriteTruncate : Mode
      ReadAppend        : Mode


    readFile  : String -> IO (Either FileError String)
    writeFile : (path : String) -> (contents : String) -> IO (Either FileError ())

    data FileError : Type
      FileReadError    : FileError
      FileWriteError   : FileError
      FileNotFound     : FileError
      PermissionDenied : FileError
      GenericFileError : Int -> FileError

    openFile  : (name : String) -> (mode : Mode) -> IO (Either FileError File)
    fGetLine  : (h : File) -> IO (Either FileError String)
    fPutStr   : (h : File) -> (str : String) -> IO (Either FileError ())
    fEOF      : File -> IO Bool 
    closeFile : File -> IO ()

интерфейсы и их имплементации

ключевое слово interface определяет блок, содержащий обязательные сигнатуры класса, а ключевое слово implementation определяет блок, в котором прописаны реализации. чтобы определить реализацию класса, нужно задать все методы, указанные в интерфейсе этого класса. реализация может быть и расширена - то есть включать не только обязательные, но и дополнительные методы

для данного типа может быть определена лишь одна реализация интерфейса, а если все же нужны разные реализации, то можно их сделать именованными:

    [myord] Ord Nat where
      compare Z (S n)     = GT
      compare (S n) Z     = LT
      compare Z Z         = EQ
      compare (S x) (S y) = compare @{myord} x y

    λΠ> :let testList : List Nat
       testList : List Nat
    λΠ> :let testList = [3,4,1]
    λΠ> show (sort testList)
      "[sO, sssO, ssssO]" : String
    λΠ> show (sort @{myord} testList)
      "[ssssO, sssO, sO]" : String

декларации реализаций могут иметь ограничения, которые записываются в скобках, через запятую. аргументами должны быть конструкторы (типов или данных), переменные или константы. нельзя определить реализацию для функции

два элиминатора

   maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b 

   either : (f : Lazy (a -> c)) -> (g : Lazy (b -> c)) -> (e : Either a b) -> c