Idrisの型 - mrsekut-p

Idrisの型

Idrisの型

とくにHaskellと異なるもののみ

型の定義が:

Haskellと異なってて、Elmと同じ

code:idr

main : IO()

Type

kindの*みたいなやつ

Ptr

ポインタの型

リスト型

code:idr

data List a = Nil | (::) a (List a)

リストの連結は::

自然数型

code:idr

data Nat = Z | S Nat

NatやZやSは組み込みの型mrsekut.icon

和を計算する

code:idr

plus : Nat -> Nat -> Nat

plus Z y = y

plus (S k) y = S (plus k y)

ペアノの公理をやっている

標準の演算子+などは使わずに定義している

plusを実行する

数値と自然数型、どちらを引数にとっても同様に演算結果が得られる

code:idr

Idris> plus 2 3

5 : Nat

Idris> plus (S (S Z)) 3

5 : Nat

NatやSやZは組み込みの型なので自動的に自然数として表示される

Haskellでも全く同様に定義できるが、自動的に自然数に変換されるのがミソ

参考

Types and Functions — Idris 1.3.3 documentation

Vect型

import Data.Vect

code:idr

data Vect : Nat -> Type -> Type where

Nil : Vect Z a

(::) : a -> Vect k a -> Vect (S k) a

要素数を保持するVector型

codata宣言

http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#codata-types

無限再帰ができる

code:idr

codata Stream : Type -> Type where

(::) : (e : a) -> Stream a -> Stream a

内部でInf型に変換される

タプル型

MkPair a b

MkPairは組み込みの型

MkPair 1 2は、(1,2)と書いても同じ

{}を使って型の明示ができる

http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#vectors

Haskellの、内部で::を使って明示するのとだいたい同じ

型宣言に名前を付けられる

e.g. index : (i:Fin n) -> (xs:Vect n a) -> a

TSみたいだねmrsekut.icon

using

http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#using-notation

{}を使って暗黙の引数を書けるが、ごちゃごちゃしてくる

usingを使ってブロックにすると見やすくなる

code:idr

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

data IsElem : a -> Vect n a -> Type where

Here : IsElem x (x :: xs)

There : IsElem x xs -> IsElem x (y :: xs)