で、そういったことをSubtypeで表現していけばいいかな、と思ったんですが
そういえばSubtypeを定義する式ってでてきたっけな？と思い当たりました
う、出てきてない
define-typeは既存の型に別名をつけるだけなので
ゲーデル数は数である、列はゲーデル数である、とやっても
結局ゲーデル数と数を区別することはできず
列を渡すべきところでゲーデル数を渡してしまった、みたいなことを
チェックすることはできそうにありません

しかしぐぐってみるとdefine-new-subtypeというのが出てきました
GuideではなくReferenceに掲載されていてしかもExperimental Featuresだと
むう
もっと基本的な機能かと思いましたが

リリースノートを確認してみたところRacket 6.3で実装されたようです
PLT SchemeのころからTyped Schemeっていうのがあったらしいことを考えると
比較的新しい機能なんですね

まあいいか
ではちょっと練習

#lang typed/racket

(define-new-subtype GNumber (gnumber Natural))
(define-new-subtype GSequence (gsequence GNumber))

(define c0 (gnumber 1))
(define s1 (gsequence (gnumber 2)))

(: number-func (-> Natural Natural))
(define (number-func x)
  (* x 2))

(number-func 0)
(number-func c0)
(number-func s1)

(: gnumber-func (-> GNumber GNumber))
(define (gnumber-func x)
  (gnumber (* x 3)))

; (gnumber-func 0) <- Error
(gnumber-func c0)
(gnumber-func s1)

(: sequence-func (-> GSequence GSequence))
(define (sequence-func x)
  (gsequence (gnumber (* x 4))))

;(sequence-func 0) <- Error
;(sequence-func c0) <- Error
(sequence-func s1)

やりたいことはできそうな感じがしてきました

2017-11-24

Typed Racketのお勉強 (12)

racket

7 Optimization in Typed Racket

Typed Racketは型の情報を活かして最適化を行います

最適化を止めるには#lang typed/racket #:no-optimizeを使う
RealよりもFloatといったように、型を具体的に指定すると効果的
リストがnullでないことがわかっている場合は明示してやるとnullチェックが省略される

たとえば整数2個のリストだとわかっていれば

(: sum2 (-> (Listof Integer) Integer))
(define (sum2 l) (+ (car l) (cadr l)))

((Listof Integer)は0個以上のIntegerのリスト)
よりも

(: sum2 (-> (List Integer Integer) Integer))
(define (sum2 l) (+ (car l) (cadr l)))

の方がいいということですね
Vectorも同様
といってもStructでいいケースではStructを使ったほうが適切で速くなります

2017-11-23

Typed Racketのお勉強 (11)

racket

6 Typed-Untyped Interaction

Typedじゃない普通のRacketの関数からTyped Racketの関数は普通に呼べます
Typed RacketからRacketの関数を呼ぶにはrequire/typedで型を指定してやります

#lang racket

(provide (struct-out pt)
         distance)

(struct pt (x y))

(define (distance p1 p2)
  (sqrt (+ (sqr (- (pt-x p2) (pt-x p1)))
           (sqr (- (pt-y p2) (pt-y p1))))))

ここで定義されたでdistanceをTyped Racketから呼ぶには以下のように書きます
(chap06-01-distance.rktは上のファイル名)

(require/typed "chap06-01-distance.rkt"
               [#:struct pt ([x : Real] [y : Real])]
               [distance (-> pt pt Real)])

実行

> (distance (pt 3 5) (pt 7 0))
- : Real
6.4031242374328485

自分の作ったファイルだけでなく標準ライブラリからも同様にしてrequire/typedできます

Typed RacketからRacketの関数を呼ぶ場合、Contractを用いて型のチェックが
行われるため、場合によってはオーバーヘッドが発生するので注意、だそうです

kb84tkhrのブログ

何を書こうか考え中ですあ、あと組織とは関係ないってやつです個人的なやつ

「ちょっと残業」

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (34)

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (33)

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (32)

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (31)

Typed Racketのお勉強 (12)

7 Optimization in Typed Racket

Typed Racketのお勉強 (11)

6 Typed-Untyped Interaction